[GHC] #14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)

19 Feb 2018

      #14822: -XQuantifiedConstraints: Turn term-level entailments (:-) into constraints
(=>)
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints, wipT2893    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This code works fine:

 {{{#!hs
 {-# 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?

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14822
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler