3

If I have the method:

proveBar :: forall x . SingI x => Dict (Barable (Foo x))
proveBar = ...

Then how do I pass this as the context to:

useBar :: forall foo . (forall x. SingI x => Barable (foo x)) => ...
useBar = ...

binding foo to Foo ?

Dict is defined here https://hackage.haskell.org/package/constraints-0.10.1/docs/Data-Constraint.html#g:2

dspyz
  • 5,280
  • 2
  • 25
  • 63
  • What's the scope of that `foo`? Is it the signature of `useBar` or its first parameter? – Fyodor Soikin Dec 27 '18 at 18:47
  • Added `forall`s to clarify – dspyz Dec 27 '18 at 18:48
  • I think the question is clearer now. – dspyz Dec 27 '18 at 18:51
  • Well, that totally looks like it should "just work" - `useBar proveBar`. The caller of `useBar` chooses `foo`, and by passing in `proveBar` you'd be choosing `Foo`. Are you getting errors? – Fyodor Soikin Dec 27 '18 at 18:51
  • It's not an argument it's a context so I don't have any way to pass it explicitly. Also notice that the `Dict` has vanished. – dspyz Dec 27 '18 at 18:53
  • Ooooooh, I didn't notice the fat arrow, sorry. – Fyodor Soikin Dec 27 '18 at 18:54
  • I don't think I quite understand it though. If `Barable (Foo x)` exists for every `x` anyway (otherwise, how would `proveBar` work?), shouldn't you be able to just `useBar @Foo`? – Fyodor Soikin Dec 27 '18 at 18:59
  • `GHC` isn't smart enough to find `SingI x => Barable (Foo x)` on its own which is why I need to write the `proveBar` function myself. – dspyz Dec 27 '18 at 19:04
  • Example: `instance KnownNat (Length xs) => Barable xs` (letting `xs` be a type-level list) – dspyz Dec 27 '18 at 19:06
  • This does indeed follow from `SingI xs`, but `GHC` won't just pick it out of the blue. – dspyz Dec 27 '18 at 19:07
  • 1
    What is the `Dict` type here? Can you show its definition? And, indeed, can you show the implementations of your two functions? – Alexis King Dec 27 '18 at 19:37
  • I've been trying to construct a MWE that compiles and it's turning out to be a lot harder than I thought. Basically, the client is supposed to have a type-level list of data-structures which are persisted, but this list is _parameterized_ over the type of foreign keys which is backend-specific. In practice this list should always be concrete so `GHC` can infer everything it needs, but in my `QuickCheck` test I want to arbitrarily generate it so I need to pack up all the relevant constraints somewhere. This is further complicated by the monad having an associated phantom type like `ST` does. – dspyz Dec 27 '18 at 21:07
  • I'll have to come back to this next week when I have more time. Sorry. – dspyz Dec 27 '18 at 21:07
  • @AlexisKing `Dict` is a GADT that witnesses the existence of a constraint, which at runtime means the presence of the dictionary, hence the name. It's [from the `constraints` package](https://www.stackage.org/haddock/lts-13.0/constraints-0.10.1/Data-Constraint.html#t:Dict). – Fyodor Soikin Dec 27 '18 at 21:40
  • Ah, of course; I had forgotten about `constraints`. Still, this question confuses me. I can’t imagine a definition for `proveBar` that wouldn’t be better written as an instance declaration `instance forall x. SingI x => Barable (Foo x)`, since even `constraints` doesn’t allow local (non-coherent) instances. Some top-level instance declaration of a similar shape to the one above *must* exist in order for `proveBar` to typecheck, right? – Alexis King Dec 27 '18 at 22:49
  • @AlexisKing I don't think it necessarily has to. `proveBar` could work at value level via singletons and elimination functions. – Fyodor Soikin Dec 27 '18 at 23:38
  • @FyodorSoikin Yes, I suppose if you bring singletons in (which, to be fair, the OP clearly has), many bets are off. I’d still like to see a MVCE, though. :) – Alexis King Dec 27 '18 at 23:40

1 Answers1

1

You can't with what you've got.

In order to use useBar with foo ~ Foo you need evidence that (forall x. SingI x => Barable (Foo x)).

Pattern matching on proveBar won't work, because by the time you match Dict, x is no longer universally qualified; you've constrained x to be a particular (unspecified) type.

What you really need is to pattern match something of type Dict (forall x. SingI x => Barable (Foo x)), but this type isn't currently supported by GHC:

• Illegal polymorphic type: forall x. SingI x => Barable (Foo x)
  GHC doesn't yet support impredicative polymorphism
• In the type signature: proveBar' :: Dict (forall x. SingI x => Barable (Foo x))

If instead you had evidence of the form

proveBar :: SingIBarable Foo

data SingIBarable foo where
  SingIBarable :: (forall x. SingI x => Barable (foo x)) -> SingIBarable foo

Then you'd be able to use useBar by pattern matching on proveBar.

rampion
  • 87,131
  • 49
  • 199
  • 315