Use of Assert in Data.Type.Ord discards crucial evidence

Summary

The constraints exposed by Data.Type.Ord only restrict and do not provide.

Rewriting them simply and directly without Assert yields variants that do both, demonstrating that the issue is a regression introduced in !6066 (closed) (see change).

Steps to reproduce

Run ghc NoProvide.hs, where:

NoProvide.hs

{-# LANGUAGE ExplicitNamespaces, DataKinds, AllowAmbiguousTypes #-}

module NoProvide where

import Data.Type.Ord (Compare, type (<=?), type (>=?))
import qualified Data.Type.Ord as Base


type a <  b = Compare a b ~ LT
type a >  b = Compare a b ~ GT
type a <= b = (a <=? b) ~ True
type a >= b = (a >=? b) ~ True


type p ==> q = forall r. (q => r) -> (p => r)

forwardsLt :: (a < b) ==> (a Base.< b)
forwardsLt r = r

backwardsLt :: (a Base.< b) ==> (a < b)
backwardsLt r = r

forwardsLeq :: (a <= b) ==> (a Base.<= b)
forwardsLeq r = r

backwardsLeq :: (a Base.<= b) ==> (a <= b)
backwardsLeq r = r

Expected behavior

The reproducer should compile without error. Alas, it fails on the backwards directions:

NoProvide.hs:21:17: error: [GHC-05617]
    • Could not deduce ‘Compare a b ~ LT’ arising from a use of ‘r’
      from the context: a Base.< b
        bound by the type signature for:
                   backwardsLt :: ((a < b) => r) -> (a Base.< b) => r
        at NoProvide.hs:21:1-17
    • In the expression: r
      In an equation for ‘backwardsLt’: backwardsLt r = r
    • Relevant bindings include
        r :: (a < b) => r (bound at NoProvide.hs:21:13)
        backwardsLt :: ((a < b) => r) -> (a Base.< b) => r
          (bound at NoProvide.hs:21:1)
   |
21 | backwardsLt r = r
   |                 ^

NoProvide.hs:27:18: error: [GHC-05617]
    • Could not deduce ‘Base.OrdCond (Compare a b) True True False
                        ~ True’
        arising from a use of ‘r’
      from the context: a Base.<= b
        bound by the type signature for:
                   backwardsLeq :: ((a <= b) => r) -> (a Base.<= b) => r
        at NoProvide.hs:27:1-18
    • In the expression: r
      In an equation for ‘backwardsLeq’: backwardsLeq r = r
    • Relevant bindings include
        r :: (a <= b) => r (bound at NoProvide.hs:27:14)
        backwardsLeq :: ((a <= b) => r) -> (a Base.<= b) => r
          (bound at NoProvide.hs:27:1)
   |
27 | backwardsLeq r = r
   |                  ^

Environment

• GHC version used: 9.10.1