id summary reporter owner description type status priority milestone component version resolution keywords cc os architecture failure testcase blockedby blocking related differential wikipage
13621 Problems with injective type families Iceland_jack "{{{#!hs
{-# 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:
{{{#!hs
data F :: Cat Type where
F :: (IB a -> a) -> F (IB a) a
}}}
but it gives
{{{#!hs
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`?" feature request new normal Compiler 8.0.1 InjectiveFamilies Unknown/Multiple Unknown/Multiple None/Unknown