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

Question

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.

Answer 1

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.