[Haskell-cafe] Type family signatures

[Simon Peyton-Jones]

David is right that the program should be rejected.  To be concrete, as he suggests, suppose
  type instance Fam Int = Bool
  type instance Fam Char = Bool

Now suppose that 'unwrap' did typecheck. Then we could write: 
  x :: Fam Int
  x = GADT 3 True

  y :: (Char, Bool)
  y = unwrap x

Voila!  We started with an Int (3), and managed to return it as the first component of a pair of type (Char,Bool).   


Ryan's explanation of the type checking process is accurate, but I agree that the error message is horrible.  Dimitrios and I are working on a better version of the type checker that will say something more helpful, like
	Cannot deduce (a ~ a1) from (Fam a ~ Fam a1)
which is a lot more useful.

Nice example, thank you.

Simon

| -----Original Message-----
| From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On
| Behalf Of Ryan Ingram
| Sent: 18 August 2009 21:56
| To: Thomas van Noort
| Cc: Haskell Cafe
| Subject: Re: [Haskell-cafe] Type family signatures
| 
| On Mon, Aug 17, 2009 at 12:12 AM, Thomas van Noort<thomas at cs.ru.nl> wrote:
| > Somehow I didn't receive David's mail, but his explanation makes a lot of
| > sense. I'm still wondering how this results in a type error involving rigid
| > type variables.
| 
| "rigid" type means the type has been specified by the programmer somehow.
| 
| Desugaring your code a bit, we get:
| 
| GADT :: forall a b. (b ~ Fam a) => a -> b -> GADT b
| 
| Notice that this is an existential type that partially hides "a"; all
| we know about "a" after unwrapping this type is that (Fam a ~ b).
| 
| unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
| unwrap (GADT x y) = (x,y)
| 
| So, the type signature of unwrap fixes "a" and "b" to be supplied by
| the caller.  Then the pattern match on GADT needs a type variable for
| the existential, so a new "a1" is invented.  These are rigid because
| they cannot be further refined by the typechecker; the typechecker
| cannot unify them with other types, like "a1 ~ Int", or "a1 ~ a".
| 
| An example of a non-rigid variable occurs type-checking this expression:
| 
| foo x = x + (1 :: Int)
| 
| During type-checking/inference, there is a point where the type environment is:
| 
| (+) :: forall a. Num a => a -> a -> a
| 
| b :: *, non-rigid
| x :: b
| 
| c :: *, non-rigid
| foo :: b -> c
| 
| Then (+) gets instantiated at Int and forces "b" and "c" to be Int.
| 
| In your case, during the typechecking of unwrap, we have:
| 
| unwrap :: forall a b. (b ~ Fam a) => GADT b -> (a,b)
|     a :: *, rigid
|     b :: *, rigid
|     (b ~ Fam a)
| 
|     -- From the pattern match on GADT:
|     a1 :: *, rigid
|     x :: a1
|     y :: b
|     (b ~ Fam a1)
| 
| Now the typechecker wants to unify "a" and "a1", and it cannot,
| because they are rigid.  If one of them was still open, we could unify
| it with the other.
| 
| The type equalities give us (Fam a ~ Fam a1), but that does not give
| us (a ~ a1).  If Fam was a data type or data family, we would know it
| is injective and be able to derive (a ~ a1), but it is a type family,
| so we are stuck.
| 
|   -- ryan
| _______________________________________________
| Haskell-Cafe mailing list
| Haskell-Cafe at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-cafe