-XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)

This code works fine:

{-# Language TypeOperators, RankNTypes, KindSignatures, GADTs, DataKinds, MultiParamTypeClasses, FlexibleInstances, ConstraintKinds, ScopedTypeVariables #-}

import Data.Kind

-- 'constraints' machinery
data Dict c where
  Dict :: c => Dict c

newtype a :- b = Sub (a => Dict b) -- entailment

-- 'singletons' machinery
data SBool :: Bool -> Type where
  SFalse :: SBool 'False
  STrue  :: SBool 'True

class    SBoolI (bool::Bool) where sbool :: SBool bool
instance SBoolI 'False       where sbool = SFalse
instance SBoolI 'True        where sbool = STrue

-- VVV Example VVV
class    Funny (b::Bool) (b'::Bool)
instance Funny 'False b'
instance Funny 'True  'True
instance Funny 'True  'False

proof :: forall b b'. (SBoolI b, SBoolI b') :- Funny b b'
proof = Sub (case (sbool :: SBool b, sbool :: SBool b') of
  (SFalse, _)      -> Dict
  (STrue,  SFalse) -> Dict 
  (STrue,  STrue)  -> Dict)
-- ^^^ Example ^^^

What I'm interested in is the entailment:

Singletons for b and b' entail Funny b b'. This is witnessed by proof.

Given that we have a branch for -XQuantifiedConstraints, it is tantalizing to convert this into an implication constraint (SBoolI b, SBoolI b') => Funny b b'.

Is such a thing sensible (wrt coherence) and if so is it at all possible to do this on WIPT2893?

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture