further mysteries of unification with constrained higher-rank types

[matthewleon]

I think this is a bug, but I'm not 100% sure. The bug might just be in my understanding of the compiler's unification strategy for these types. If so, I apologize and will post further queries in a more appropriate forum. As it stands, though, the behavior below is at least... Perplexing.

module Main where

import Data.Typelevel.Num.Ops (class Pred)
import Data.Typelevel.Num.Reps (D0, D1)

data List s a = Nil | Cons a (forall s'. Pred s s' => List s' a)

cons :: forall s a. a -> (forall s'. Pred s s' => List s' a) -> List s a
cons x xs = Cons x xs
infixr 6 cons as :

empty :: forall a. List D0 a
empty = Nil

singleton :: forall a. a -> List D1 a
singleton x = x : empty

Compilation errors on the definition of singleton. Here is the verbose error:

  Could not match type
      
    D0
      
  with type
       
    s'3
       

while trying to match type D0
  with type s'3
while trying to match type List D0
  with type List s'3
while trying to match type List D0 t4
  with type List s'3 a0
while checking that type forall a. List D0 a
  is at least as general as type List s'3 a0
while checking that expression empty
  has type List s'3 a0
while checking that expression empty
  has type Pred t1 s'3 => List s'3 a0
while checking that expression empty
  has type forall s'. Pred t1 s' => List s' a0
while applying a function cons x
  of type (forall s'. Pred t1 s' => List s' t2) -> List t1 t2
  to argument empty
while checking that expression (cons x) empty
  has type List D1 a0
while checking that expression \x ->           
                                 (cons x) empty
  has type a0 -> List D1 a0
while checking that expression \x ->           
                                 (cons x) empty
  has type forall a. a -> List D1 a
in value declaration singleton

where a0 is a rigid type variable
        bound at line 16, column 1 - line 16, column 19
      s'3 is a rigid type variable
        bound at line 16, column 19 - line 16, column 19
      t2 is an unknown type
      t1 is an unknown type
      t4 is an unknown type

Not only does it seem to me that these types should unify, but that D0 is the only type the could unify, due to the Pred constraint applied to D1. I have a slight suspicion that my brain might be clouded by Prolog, though.

[matthewleon]

Something tells me that the evil part is in the following step:

while checking that type forall a. List D0 a
  is at least as general as type List s'3 a0

D0 is indeed not "at least as general as" s'3. On the contrary. But this seems like reverse logic. What we should be checking, it seems, is that D0 is subsumed by s'3.

[paf31]

Why not

cons :: forall s s' a. Pred s s' => a -> List s' a -> List s a

?

Edit: this is the problem, I think. s' in Cons should be existential, not universal.

[paf31]

Here is another way you can solve this: http://try.purescript.org/?gist=7a7f8b65e0db2757508dfee38ddb07ed

This is safe because the functional dependency n -> p on Pred means that the APred type constructor is well-defined.)

[matthewleon]

When I copy-paste your suggestion, I still get the same error, I think because now the definition of cons clashes with that of Cons.

How does one make the s' in Cons existential rather than universal? Are there some type gymnastics with purescript-exists that do this sort of thing? To my naïve eyes, it looks existential the way it is now because of its position inside the parens of the constructor.

(I will mess around with purescript-exists and see if it does the trick now).

As for the other example, thank you. I see that it works. The APred trick feels weirdly hackish to me, but that might be a problem with my unfamiliarity with these kind of type techniques.

On a more broad note, I wonder if you think these kinds of things are a worthwhile avenue to pursue, generally speaking, or if I'm likely to run into a lot of dead ends and cryptic error messages.

Lots of questions, I know... But I do find your responses here very helpful.

[paf31]

If you want s' to be existential in Cons, you can use a double-negation encoding:

data List s a = Nil | Cons a (forall r. (forall s'. Pred s s' => List s' a -> r) -> r)

(http://try.purescript.org/?gist=351b6a383d27fb0396ec286591f2f887)

but it's not as efficient and it doesn't have the same representation at runtime. That's why purescript-exists uses unsafe-coerce under the hood. I think it's fine to do so as long as we can decide that it's safe because we chose the representation, or because of some fundep, etc.

I think this sort of thing is worth pursuing, but coming up with a good API with good type errors can be challenging :)

[matthewleon]

Oh wow...

Okay, thanks for the tip on that. I wouldn't have thought of it. I'm going to close this. This has been very educational :). If you have any additional external resources for learning these kind of tricks that you would recommend off the top of your head, I'd very much appreciate them. Obviously Haskell-land would be the place to turn, but it seems that FunDeps are no longer the tool of choice for higher-rank tricks over there.