Re: [GHC] #14937: QuantifiedConstraints: Reify implication constraints from terms lacking them

7 Nov 2018

      #14937: QuantifiedConstraints: Reify implication constraints from terms lacking
them
-------------------------------------+-------------------------------------
        Reporter:  Bj0rn             |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #14822, #15635    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Bj0rn):

 Here's a motivating example where I wish that I was able to show the
 compiler that one (quantified) constraint implies another. In this
 example, I'm using the `singletons` library. The
 `Data.Singletons.TypeLits` module contains

 {{{#!hs
 data instance Sing (n :: Nat) = KnownNat n => SNat

 instance KnownNat n => SingI n where
   sing = SNat
 }}}

 where the compiler learns of the implication `forall n. KnownNat n =>
 SingI n`. However the reverse implication `forall n. SingI n => KnownNat
 n` is also true as evidenced by:

 {{{#!hs
 data Dict :: Constraint -> Type where
     Dict :: c => Dict c

 singIToKnownNat :: forall n. SingI n => Dict (KnownNat n)
 singIToKnownNat = case sing @n of SNat -> Dict
 }}}

 The crux is that there's is no way to rephrase `singIToKnownNat` in terms
 of constraint implication:

 {{{#!hs
 singIImpliesKnownNat :: forall r. ((forall n. SingI n => KnownNat n) => r)
 -> r
 singIImpliesKnownNat a = undefined          -- Can't implement this?
 }}}

 What this ticket asks for is some way to write a correct definition of
 things like `singIImpliesKnownNat`. Something similar to the definition of
 `singIToKnownNat`, I would imagine.

 Here's the full example code:

 {{{#!hs
 -- GHC 8.6.2, Singletons 2.5

 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE QuantifiedConstraints #-}

 module ReifyImplications where

 import Data.Kind
 import GHC.TypeNats
 import Data.Singletons
 import Data.Singletons.TypeLits
 import Data.Type.Equality

 data EmptyVec :: Nat -> Type where
     EmptyVec :: EmptyVec 0

 instance KnownNat n => Read (EmptyVec n) where
     readsPrec _ "EmptyVec" =
         case sameNat @n @0 Proxy Proxy of
             Just Refl -> [(EmptyVec, "")]
             Nothing -> []

 data Some1 :: (k -> Type) -> Type where
     Some1 :: Sing a -> f a -> Some1 f

 readKnowingTypeIndex ::
     forall k (f :: k -> Type). (forall x. SingI x => Read (f x)) =>
         SomeSing k -> String -> Some1 f
 readKnowingTypeIndex (SomeSing s) str =
     Some1 s $ withSingI s $ read str

 readKnowingNat ::
     forall (f :: Nat -> Type). (forall n. KnownNat n => Read (f n)) =>
         SomeSing Nat -> String -> Some1 f
 readKnowingNat (SomeSing (SNat :: Sing a)) str =
     Some1 (SNat @a) $ read str              -- Can't write this in terms
 of readKnowingTypeIndex?

 ev :: SomeSing Nat -> Some1 EmptyVec
 --ev s = readKnowingTypeIndex s "EmptyVec"  -- Could not deduce (KnownNat
 x).
 --ev s = readKnowingNat s "EmptyVec"        -- OK, but this doesn't work
 on every kind. Only Nat.

 singIImpliesKnownNat :: forall r. ((forall n. SingI n => KnownNat n) => r)
 -> r
 singIImpliesKnownNat a = undefined          -- Can't implement this?

 ev s =
     singIImpliesKnownNat $
         readKnowingTypeIndex s "EmptyVec"   -- OK, if singIImpliesKnownNat
 was real.

 -- Now, this is easy to implement. But it's not practically usable in the
 definition of `ev`.
 data Dict :: Constraint -> Type where
     Dict :: c => Dict c

 singIToKnownNat :: forall n. SingI n => Dict (KnownNat n)
 singIToKnownNat = case sing @n of SNat -> Dict

 -- Bonus: readKnowingNat written in terms of readKnowingTypeIndex
 readKnowingNat' ::
     forall (f :: Nat -> Type). (forall n. KnownNat n => Read (f n)) =>
         SomeSing Nat -> String -> Some1 f
 readKnowingNat' s str =
     singIImpliesKnownNat $
         readKnowingTypeIndex s str
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14937#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler