Closed type families, apartness, and occurs check

[Brandon Moore]

>From the user manual, it sounds like a clause of a closed type family should be rejected once no subsitution of the type could make it unify with the clause. If so, it doesn't seem to do an occurs check:


type family IsEq a b :: Bool where
  IsEq a a = True
  IsEq a b = False


> :kind! forall a . IsEq a a
forall a . IsEq a a :: Bool
= forall (a :: k). 'True
> :kind! forall a . IsEq a [a]
forall a . IsEq a [a] :: Bool
= forall a. IsEq a [a]


I came across this while trying to using Generics to find the immediate children of a term - this sort of non-reduction happens while comparing a type like (Term var) with a constructor argument of type var.


Brandon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140702/c1b54f88/attachment.html>