[GHC] #8669: Closed TypeFamilies regression

[GHC]

#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