[GHC] #8669: Closed TypeFamilies regression

[GHC]

#8669: Closed TypeFamilies regression
--------------------------+------------------------------------------------
       Reporter:  merijn  |             Owner:
           Type:  bug     |            Status:  new
       Priority:  high    |         Milestone:
      Component:          |           Version:  7.7
  Compiler                |  Operating System:  Unknown/Multiple
       Keywords:          |   Type of failure:  Incorrect result at runtime
   Architecture:          |         Test Case:
  Unknown/Multiple        |          Blocking:
     Difficulty:          |
  Unknown                 |
     Blocked By:          |
Related Tickets:          |
--------------------------+------------------------------------------------
 I first played around with closed typefamilies early 2013 and wrote up the
 following simple example

 {{{
 {-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies,
 TypeOperators #-}

 import GHC.Prim (Constraint)

 type family Restrict (a :: k) (as :: [k]) :: Constraint
 type instance where
     Restrict a (a ': as) = (a ~ "Oops! Tried to apply a restricted type!")
     Restrict x (a ': as) = Restrict x as
     Restrict x '[] = ()

 foo :: Restrict a '[(), Int] => a -> a
 foo = id
 }}}

 This worked fine, functioning like `id` for types other than `()` and
 `Int` and returning a type error for `()` and `Int`.

 After hearing comments that my example broke when the closed type families
 syntax changed I decided to update my version of 7.7 and change the code
 for that. The new code is:

 {{{
 {-# LANGUAGE ConstraintKinds, DataKinds, PolyKinds, TypeFamilies,
 TypeOperators #-}

 import GHC.Prim (Constraint)

 type family Restrict (a :: k) (as :: [k]) :: Constraint where
     Restrict a (a ': as) = (a ~ "Oops! Tried to apply a restricted type!")
     Restrict x (a ': as) = Restrict x as
     Restrict x '[] = ()

 foo :: Restrict a '[(), Int] => a -> a
 foo = id
 }}}

 This code is accepted by the compiler just fine, but the `Constraint` gets
 thrown out. When querying ghci for the type of `foo` the following is
 returned:

 {{{
 λ :t foo
 foo :: a -> a
 λ :i foo
 foo :: (Restrict a '[(), Int]) => a -> a
 }}}

 Additionally, in the recent 7.7 `foo ()` returns `()` rather than a type
 error. After some playing around this seems to be caused by the "(a ~
 "Oops! Tried to apply a restricted type!")" equality constraint. It seems
 GHC decides that it doesn't like the fact that types with a polymorphic
 kind and `Symbol` kind are compared. Leading it to silently discard the
 `Constraint`.

 This raises two issues:
   1) This should probably produce an error, rather than silently
 discarding the `Constraint`
   2) A better way to produce errors in type families is needed, personally
 I would love an "error" `Constraint` that takes a `String`/`Symbol` and
 never holds, producing it's argument `String` as type error (This would
 remove the need for the hacky unification with `Symbol` to get a somewhat
 relevant type error).

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8669>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler