Can I prove that (forall x. Coercible (a x) (b x)) implies Coercible a b?

user_9859 0
Viewed 120

I'm manipulating proofs of coercibility:

data a ~=~ b where
  IsCoercible :: Coercible a b => a ~=~ b
infix 0 ~=~

sym :: (a ~=~ b) -> (b ~=~ a)
sym IsCoercible = IsCoercible

instance Category (~=~) where 
  id = IsCoercible
  IsCoercible . IsCoercible = IsCoercible

coerceBy :: a ~=~ b -> a -> b
coerceBy IsCoercible = coerce

I can trivially prove Coercible a b => forall x. Coercible (a x) (b x)

introduce :: (a ~=~ b) -> (forall x. a x ~=~ b x)
introduce IsCoercible = IsCoercible

But not the converse, (forall x. Coercible (a x) (b x)) => Coercible a b) isn't quite as free:

eliminate :: (forall x. a x ~=~ b x) -> (a ~=~ b)
eliminate IsCoercible = IsCoercible
{-
   • Could not deduce: Coercible a b
        arising from a use of ‘IsCoercible’
      from the context: Coercible (a x0) (b x0)
        bound by a pattern with constructor:
                   IsCoercible :: forall k (a :: k) (b :: k).
                                  Coercible a b =>
                                  a ~=~ b,
                 in an equation for ‘eliminate’
-}

I'm fairly certain my claim is valid (though I'm open to being disproven), but I'm not having any bright ideas as to how to prove it within Haskell short of unsafeCoerce.

coercion haskell
1 Answers

No, you can't. As Dominique Devriese and HTNW hint in their comments, GHC doesn't admit that inference at all. This more demanding version won't compile:

{-# language QuantifiedConstraints, RankNTypes #-}

import Data.Coerce
import Data.Type.Coercion

eliminate :: (forall a. Coercible (f a) (g a)) => Coercion f g
eliminate = Coercion

Your version is even more doomed. To pattern match on the polymorphic Coercion (or ~=~) argument, it must be instantiated to a particular type. GHC will instantiate it to f Any ~=~ g Any, which is then monomorphic and therefore doesn't prove what you want it to. Since GHC Core is typed, that won't fly.

Side note: I find it intensely frustrating that there's no way to write

f :: (forall a. c a :- d a)
  -> ((forall a. c a => d a) => r)
  -> r
user_14776670
Related