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

mentioned in issue #10833

changed weight to 5

added Tbug Trac import typechecker labels

changed title from GHC is oblivious to injectivity when a type family is used in a GADT type to GHC is oblivious to injectivity when solving an equality constraint

gelisam points out an even simpler failing example that doesn't involve GADTs. Even worse, it's cited as an example that should typecheck from section 5.3 of the original injective type families paper!

{-# LANGUAGE TypeFamilyDependencies #-}

type family F a = b | b -> a

fid :: (F a ~ F b) => a -> b
fid x = x

Could not deduce: a ~ b
from the context: F a ~ F b

Example in #ticket:12199#comment:121577 should not compile yet - see #10833 for details.

Trac metadata

Trac field	Value
Related	- → #10833

added 1 deleted label

closed

This is really a duplicate of #10833.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

added TypeFamilies injective type families labels

added Pnormal label