GHC is oblivious to injectivity when solving an equality constraint

A reddit post points out a limitation of injective type families:

{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE TypeFamilyDependencies #-}

type family Foo a = b | b -> a where
  Foo Int = Bool

data Bar :: * -> * where
  Bar :: a -> Bar (Foo a)

oink :: Bar Bool -> Int
oink (Bar x) = x  -- type error

Compiling this fails with:

Could not deduce: a ~ Int
from the context: Bool ~ Foo a

Which seems odd, given that Bool ~ Foo a should imply a ~ Int by injectivity. Even if you change the type signature of oink to Bar (Foo Int) -> Int, it fails with:

Could not deduce: a ~ Int
from the context: Foo Int ~ Foo a

which makes it even more apparent that it isn't aware of the fact that Foo is injective.

Trac metadata

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