Understanding Family Types

Question

I am studying Type Families and trying to understand why I am not getting a compile-time error in a particular case.

My type family is defined as follows:

type family Typ ab :: Constraint type instance Typ (Label x) (Label y) = () 

I have two functions as shown below:

 func1 :: (Typ (Label "la") (Label "lb")) => Label "la" -> Label "lb" -> String func1 = undefined func2 :: (Typ (Label "la") String) => Label "la" -> String -> String func2 = undefined 

Both of these functions compile OK.

When I try to view the type func1 , I get the correct signature. But, when I try to view the type func2 , I get an error on error

Failed to print (Typ (Label "la") String)

Why is this so? Can someone help me understand?

Answer 1

I was able to duplicate what you described with this Label definition:

 import GHC.TypeLits (Symbol) data Label (a :: Symbol) 

And adding:

 type instance Typ (Label x) String = () 

Then provides type func2

Edit

Sorry, I misunderstood the concern. I understand that constraint feasibility testing will be delayed until func2 is used, as an instance can be added later.

For example, adding:

 func3 = func2 (undefined :: Label "la") "" 

Makes it crash during compilation.

The way I understand this is that func2 says that if you give me Label "la" and String , and the instance of Typ (Label "la") String is in scope at that time, I will give you a String . But func2 doesn't have to have an instance in sight to know what it would do with one if it were.