#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