#8669: Closed TypeFamilies regression ------------------------------------------------+-------------------------- Reporter: merijn | Owner: Type: bug | Status: closed Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: invalid | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect result at runtime | Unknown/Multiple Test Case: | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: ------------------------------------------------+-------------------------- Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: (Written before Simon's post -- I guess we think alike!) I would say that GHC's behavior in this case is correct, for the following reasons: 1. The equality operator `~` is ''homogeneous''. This means that the kinds of the types on both sides must be the same. With this in mind, here is `Restrict`, with all kind variables/arguments made explicit: {{{ type family Restrict (k :: BOX) (a :: k) (as :: [k]) :: Constraint where forall (a :: Symbol) (as :: [Symbol]). Restrict Symbol a (a ': as) = (a ~ "...") forall (k :: BOX) (x :: k) (a :: k) (as :: [k]). Restrict k x (a ': as) = Restrict k x as forall (k :: BOX) (x :: k). Restrict k x ('[] k) = () }}} In your `foo`, the variable `a` surely has kind `*`, not `Symbol`. So, the first equation of `Restrict` does not apply, and GHC correctly reduces the type family away when reporting the type of `foo`, as the constraint always reduces to `()`. 2. You suggest that GHC should produce an error here. But, there's no real way for GHC to know that you're not trying to write a ''kind-indexed'' type family, where matching on the kind really is intentional. Some possible ways forward: 1. Closed type families do full kind inference (unlike open ones), but with a twist: a kind variable used in matching must be declared in a kind annotation. Thus, if you use kind inference only, then you indeed would get an error with a definition like `Restrict`. So, unless you want a kind-indexed type family, you might be best off omitting the kind annotations. (I realize there's a good deal of value in having a kind annotation even if you don't want a kind-indexed type family, but putting in the kind variable opens you up to the possibility of silent unintended behavior in this way. I'm open to suggestions of other ways of distinguishing kind-indexed from non-kind-indexed type families!) 2. With or without kind annotations, you can do something like this: {{{ class False ~ True => Error (x :: Symbol) }}} and then use that in your first equation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8669#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler