| | /tmp/t.hs:8: | | Could not deduce `Silly a1 t' from the context (Silly a t) | | Probable fix: | | Add `Silly a1 t' | | to the the existential context of a data constructor | | arising from use of `Exist' at /tmp/t.hs:8 | | in the definition of function `applyId': Exist (Id x) | | The trouble is that | Exist :: forall a, t. Silly a t => Exist t | | Now this is an ambigous type, Sorry, I was wrong about this. The type should be data Exist a = forall t. Silly a t => Exist t Exist :: forall a, t. Silly a t => t -> Exist a So it's not ambiguous; but my other comment was right. In your example: | > applyId (Exist x) = Exist (Id x) the LHS pattern discharges the constraint (Silly a1 t), but the RHS introduces the constraint (Silly a2 t), and there's no connection between t1 and t2. Why should there be? You could give a type signature applyId :: Exist a -> Exist a and that would force them to be the same S Simon