haskellghctype-familiesinjective-function

How to help GHC infer that `Arrows (Domains func) (CoDomain func) ~ func`

Consider the Arrows, Domains and CoDomain type-families defined in the agda codebase.

Obvious to the programmer, it holds that Arrows (Domains func) (CoDomain func) ~ func. But I can't get curries (Proxy :: Proxy (Domains func)) (Proxy :: Proxy (CoDomain func)) undefined :: func through GHC's type-checker. That's because GHC isn't smart enough to infer that the combination of Domains and CoDomain is injective. Is there a way to teach GHC nonetheless? I'd imagine some case split over the IsBase predicate.

Solution

  • Would it be better for you to change Currying to be indexed by func?

    class Currying func where
  curries :: (Products (Domains func) -> CoDomain func) -> func
  uncurries :: func -> Products (Domains func) -> CoDomain func

instance Currying b => Currying (a -> b) where
  curries f a = curries (f . (,) a)
  uncurries f (a, as) = uncurries (f a) as

instance {-# OVERLAPPABLE #-} (IsBase b ~ 'True) => Currying b where
  curries f = f ()
  uncurries b _ = b

    We can also assert axioms in this way, though I'm not even sure this one is safe:

    arrowAxiom :: forall func. func :~: Arrows (Domains func) (CoDomain func)
arrowAxiom = unsafeCoerce Refl

    The equality can be put in scope by pattern matching on the axiom.