-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 |