## 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 (see [change](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6066/diffs#diff-content-95e73d0931d48e4d7a170c2b4255816dae723645)). ## Steps to reproduce Run `ghc NoProvide.hs`, where: `NoProvide.hs` ```haskell {-# 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: ```text 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