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:

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).

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