Problems with injective type families
{-# LANGUAGE GADTs, TypeInType, DataKinds, TypeFamilyDependencies #-}
import Data.Kind
type family
IB a = res | res -> a where
IB Int = Bool
IB Bool = Int
type Cat k = k -> k -> Type
data F :: Cat Type where
F :: (a -> IB a) -> F a (IB a)
data Exp :: Type -> Type where
I :: Int -> Exp Int
B :: Bool -> Exp Bool
fmap' :: F a b -> (Exp a -> Exp b)
fmap' (F f) = \case
B b -> I (f b)
I i -> B (f i)
I would have thought this should work as well, given that IB
is injective:
data F :: Cat Type where
F :: (IB a -> a) -> F (IB a) a
but it gives
fmap' :: F a b -> (Exp a -> Exp b)
fmap' (F f) = \case
B b -> I (f b)
-- c.hs:33:13: error:
-- • Could not deduce: b ~ Int
-- from the context: a ~ IB b
-- bound by a pattern with constructor:
-- F :: forall a. (IB a -> a) -> F (IB a) a,
-- in an equation for ‘fmap'’
-- at c.hs:32:8-10
-- or from: a ~ Bool
-- bound by a pattern with constructor: B :: Bool -> Exp Bool,
-- in a case alternative
-- at c.hs:33:3-5
-- ‘b’ is a rigid type variable bound by
-- the type signature for:
-- fmap' :: forall a b. F a b -> Exp a -> Exp b
-- at c.hs:31:10
-- • In the first argument of ‘I’, namely ‘(f b)’
-- In the expression: I (f b)
-- In a case alternative: B b -> I (f b)
-- • Relevant bindings include
-- f :: IB b -> b (bound at c.hs:32:10)
-- fmap' :: F a b -> Exp a -> Exp b (bound at c.hs:32:1)
-- Failed, modules loaded: none.
But if we know that a ~ Bool
(as we do from matching on B
), and we know that a ~ IB b
then by injectivity it should figure that b ~ Int
?
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |