RankNTypes issue

[iitalics]

Ran into an issue with the following (contrived) example:

(data Nop
  (nop (∀ [a] {a -> a})))
(defn ->nop : (∀ [a] {a -> Nop -> a})
  [[x (nop f)] (f x)])

The equivalent Haskell is:

data Nop = Nop (forall a. a -> a)
toNot :: a -> Nop -> a
toNot x (Nop f) = f x

Hackett complains with:

; a38218: skolem escaped its scope
;   in: a38218
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:113:4 simplify/elaborate
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:98:2 τs⇔/λ!
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:214:2 τ⇔/λ!
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:229:2 τ⇔!
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:238:2 τ⇐!
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:243:2
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:368:0
;  /home/milo/Git/hackett/hackett-lib/hackett/private/base.rkt:200:8 for-loop

Removing the outer quantification also throws the same error

(defn int-nop : {Nop -> Integer}
  [[(nop f)] (f 3)])

For some reason, Hackett really doesn't like using quantified types stored within data. The following does work:

(defn int-nop/fn : {(∀ [a] {a -> a}) -> Integer}
  [[f] (f 3)])

I'm going to guess this has something to do with unordered contexts, or maybe is just a small bug in the implementation. I'll take a look when I have some time

[lexi-lambda]

I’ve known for a while that way skolems are handled is currently very broken, though I assumed it generally erred on the side of being more permissive. I think the way skolems are added and removed from contexts it probably totally wrong, and I just didn’t put a lot of effort into making them right and coming up with good test cases. That needs to be improved, and the skolem escape error message should also be made more user-friendly when that happens (currently it’s so unreliable that I didn’t even bother).

[lexi-lambda]

Digging into this slightly, the issue seems to clearly be in the typechecking for pattern-matching. Currently, this is done with pat⇒! and pat⇐!. When pat⇒! infers the types for a match against a data constructor, it calls pat⇐! to try and ensure subpatterns have the proper types. The trouble is that pat⇐! eventually calls τ<:!, which is wrong—subsumption always instantiates quantifiers.

Currently, it requires that subpatterns’ types by subtypes of data constructors’ types. This is probably the worst possible choice, and flipping that relation makes your example typecheck. However, even flipping the subsumption relation makes pattern-matching instantiate quantifiers too early. When pattern-matching against a nop constructor, you should end up with a polymorphic binding, not a monomorphic one. Subsumption will instantiate the quantifier to a fresh unification variable, which means your binding can be used with any type, but only one (unless you explicitly force generalization by creating a local binding with a polymorphic type signature).

I think the solution is to perform some sort of simpler unification algorithm that doesn’t over-instantiate. But I haven’t taken the time to figure out exactly how that should work.

[iitalics]

An immediate solution would be to modify the pat⇐! function to recognize pattern variables rather than just calling into pat⇒!. The previous way is problematic because all pattern variables end up with τ:var^ types, which can't be instantiated to polymorphic types.

However I'm not exactly sure why it would complain about skolems "escaping" either way.