Closed TypeFamilies regression
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:
- This should probably produce an error, rather than silently discarding the
Constraint
- A better way to produce errors in type families is needed, personally I would love an "error"
Constraint
that takes aString
/Symbol
and never holds, producing it's argumentString
as type error (This would remove the need for the hacky unification withSymbol
to get a somewhat relevant type error).
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | high |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |