Opened 3 years ago

Closed 23 months ago

#12199 closed bug (duplicate)

GHC is oblivious to injectivity when solving an equality constraint

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeFamilies, InjectiveFamilies Cc: jstolarek, nfrisby
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #10833 Differential Rev(s):
Wiki Page:

Description

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.

Change History (5)

comment:1 Changed 3 years ago by RyanGlScott

Summary: GHC is oblivious to injectivity when a type family is used in a GADT typeGHC 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

comment:2 Changed 3 years ago by jstolarek

Example in #comment:1 should not compile yet - see #10833 for details.

comment:3 Changed 2 years ago by simonpj

Keywords: InjectiveFamilies added; Injective removed

comment:4 Changed 2 years ago by nfrisby

Cc: nfrisby added

comment:5 Changed 23 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

This is really a duplicate of #10833.

Note: See TracTickets for help on using tickets.