#14832: QuantifiedConstraints: Adding to the context causes failure

14823.md

Solving Trac ticket #14832:

{-# Language QuantifiedConstraints, ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, UndecidableInstances, ConstraintKinds, MultiParamTypeClasses, InstanceSigs, TypeApplications #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Coerce

data Dict c where
  Dict :: c => Dict c

class    (a => b) => Implies a b
instance (a => b) => Implies a b

type a |- b = Dict (Implies a b)

data With cls a b where
  With :: cls a b => With cls a b

type Coercion = With Coercible

class    (forall xx. rel xx xx) => Refl rel 
instance (forall xx. rel xx xx) => Refl rel 

class    (forall xx yy zz. (rel yy zz, rel xx yy) `Implies` rel xx zz) => Trans rel
instance (forall xx yy zz. (rel yy zz, rel xx yy) `Implies` rel xx zz) => Trans rel

instance (Refl rel, Trans rel) => Category (With rel) where
  id :: forall a. With rel a a
  id = With

  (.) :: forall b c a. With rel b c -> With rel a b -> With rel a c
  With . With 
    | Dict <- Dict :: (rel b c, rel a b) |- rel a c 
    = With

Testing out:

a :: With (~) a a
a = id @(With (~))

b :: With Coercible a a
b = id @(With Coercible)