#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