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

[GHC]

#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):

 I end up wishing that I could put myself in some sort of context where I
 claim that "`n` could be anything, and suppose we have `SingI n`", so that
 I'm allowed to call `singIToKnownNat @n`. In this context, the fact that
 we're able to produce a `Dict (KnownNat n)`, should prove to the compiler
 that `forall n. SingI n => KnownNat n`.

 The expression that you provide in this context would get implicitly
 pattern matched, in order to learn the constraints that can result from
 the assumption made in the context. The compiler concludes that the
 assumed constraint implies the constraints found by the implicit pattern
 match.

 I'll make up some syntax for this. Imagine a `suppose ... in ...` keyword:

 {{{#!hs
 ev :: SomeSing Nat -> Some1 EmptyVec
 ev s =
     suppose forall (n :: Nat). SingI n =>
         singIToKnownNat @n
     in
         readKnowingTypeIndex s "EmptyVec"
 }}}

 It's a funny mix of type level and expression level syntax.
 `singIToKnownNat @n` soundly returns a `Dict (KnownNat n)`, and pattern
 matching on the resulting `Dict` constructor would make us learn that for
 all `n`, `SingI n` (from the `suppose` context) implies `KnownNat n`.

 In fact this has nothing to do with `Dict`. The following would work
 equally well:

 {{{#!hs
 ev :: SomeSing Nat -> Some1 EmptyVec
 ev s =
     suppose forall (n :: Nat). SingI n =>
         sing @n
     in
         readKnowingTypeIndex s "EmptyVec"
 }}}

 since, after all, `sing @n` returns an `SNat :: Sing n`, which when
 pattern matched brings `KnownNat n` into scope.

 I don't mean to pollute language syntax. If there's a way to avoid new
 syntax, like a magical built-in function, that's preferable. It also has
 to be able to quantify over various numbers of type variables, so I don't
 think the built-in function that I proposed in the description would even
 work in this practical case.

 I'm a bit curious. When I try to write

 {{{#!hs
 suppose1 :: forall a b r. (forall x. a x => Dict (b x)) -> ((forall x. a x
 => b x) => r) -> r
 suppose1 Dict a = a
 }}}

 GHC complains already on the type signature: `Could not deduce: b x`.
 What's going on there?

 I wouldn't be surprised if it's already possible today to write something
 magical using unsafeCoerce that works for specific cases, in the style of
 Edward Kmett's `reflection` package. But that's not a long-term solution.

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