Can't create injective type family equation with TypeError as the RHS

For the longest time, I've wanted to make a type family like this injective:

type family Foo (a :: *) :: * where
  Foo Bar = Int
  Foo Baz = Char

But the problem is that Foo is defined on //all// types of kind *, so the above definition is inherently non-injective. With the introduction of TypeErrors, however, I thought I could rule out all other cases:

import GHC.TypeLits

type family Foo (a :: *) = (r :: *) | r -> a where
  Foo Bar = Int
  Foo Baz = Char
  Foo _   = TypeError ('Text "boom")

But this doesn't work, sadly:

Injective.hs:18:3: error:                                                                 
    • Type family equations violate injectivity annotation:                               
        Foo Bar = Int -- Defined at Injective.hs:18:3                                     
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

Injective.hs:20:3: error:
    • Type family equation violates injectivity annotation.
      Type variable ‘_’ cannot be inferred from the right-hand side.
      In the type family equation:
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

Injective.hs:20:3: error:
    • Type family equation violates injectivity annotation.
      RHS of injective type family equation cannot be a type family:
        Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
    • In the equations for closed type family ‘Foo’
      In the type family declaration for ‘Foo’

From GHC's perspective, TypeError is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being TypeError is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that Foo a ~ Foo b (and GHC hasn't blown up yet due to type erroring), we should be able to conclude that a ~ b.

Could this be accomplished by simply adding a special case for TypeError in the injectivity checker?

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire, jstolarek
Operating system
Architecture