Understanding type families

Question

I am learning Type Families and trying to understand why I am not getting a compile-time error under a specific case.

My type family is defined as below:

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

I have two functions as 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 these functions compile OK.

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

Could not deduce (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 definition of Label:

import GHC.TypeLits (Symbol)

data Label (a :: Symbol)

And adding:

type instance Typ (Label x) String = ()

Then provides the type of func2

Edit

Sorry I misunderstood the concern. My understanding is that checking the satisfiability of the constraint will be deferred until func2 is actually used since an instance could be added later.

For example, adding:

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

Causes it to fail at compile time.

The way I make sense of it is that func2 is saying, if you give me a Label "la" and a String and an instance of Typ (Label "la") String is in scope at the time, I'll give you a String. But func2 doesn't need to have an instance in scope to know what it would do with one if it had it.