Opened 2 years ago

Last modified 2 years ago

#13621 new feature request

Problems with injective type families

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: InjectiveFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

{-# 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?

Change History (4)

comment:1 Changed 2 years ago by goldfire

No, injectivity can't yet do this. Injectivity annotations are very much like functional dependencies, working only to do type inference. They have no representation in Core. Why not, you ask? Because I was unable to prove the soundness of doing so. But perhaps Constrained Type Families gives us a way forward here. I have yet to attempt the injectivity proof in the context of that paper, but my hunch is that it will succeed.

comment:2 Changed 2 years ago by Iceland_jack

Sounds promising, should the ticket be kept open?

comment:3 Changed 2 years ago by goldfire

Type: bugfeature request

As a feature request, sure. But don't hold your breath! :)

comment:4 Changed 2 years ago by Iceland_jack

Too late!

Note: See TracTickets for help on using tickets.