Lifting constraints is questionably correct for implicit parameters.

[dolio]

Greetings,

While fooling with implicit parameters today, I encountered an anomaly. Part of (I think) the justification of implicit parameters is that the types inform you of what they do. So, for instance:

(\() -> ?x) :: (?x :: Int) => () -> Int

depends on an implicit parameter, while:

(let ?x = 5 in \() -> ?x) :: () -> Int

does not. However, I discovered that the following:

(let ?x = 5 in \() -> ?x) :: () -> ((?x :: Int) => Int)

generates a function whose implicit parameter ?x is actually unbound, so if we let that expression be f, then:

let ?x = 4 in f ()

yields 4. By contrast, if we give the type:

(let ?x = 5 in \() -> ?x) :: (?x :: Int) => () -> Int

the ?x in the lambda expression is bound, and the implicit parameter constraint is spurious (like 5 :: (?x :: Int) => Int). This happens for definitions in which types are given, so it does not seem like it is a case of the note on monomorphism in the implicit parameters documentation. For instance:

let f :: (?x :: Int) => () -> Int
    f = let ?x = 5 in \() -> ?x
    g :: () -> ((?x :: Int) => Int)
    g = let ?x = 5 in \() -> ?x
 in let ?x = 4
     in (f (), g()) -- (5, 4)

This would arguably be fine, as the two have different types. However, GHC does not actually distinguish them. Asking the type of either will generate:

(?x :: Int) => () -> Int

Instead of the one with the higher-rank (so to speak) constraint.

I get this behavior using 6.12.1, but it seems unlikely that it would have changed in the 6.12 series.

Strictly speaking, I'm not sure I can call this a bug. Due to context weakening, there's probably no way to unambiguously clarify using types which values are genuinely dependent on implicit parameters, and which are not (similar to ask versus local (const 5) ask in Reader). However, it seems odd that the type annotations make a difference, yet are not subsequently distinguished. It's also conceivable that the () -> ((?x :: Int) => Int) behavior is unintentional. I am unsure which, if any, of these resolutions is appropriate.

So, instead, I'll call this a proposal, that we determine whether this is the intended behavior (feel free to promote to a bug if it is decided that something needs to be fixed, however). :)

[simonpj]

I agree that it's most unexpected that f and g behave differently in your last example. I would not say it's the expected behaviour! I'll check this in the new type inference engine when it's done. Thanks for pointing it out.

Simon

[ezyang]

Some more interesting behavior:

Prelude> let ?p = 5 in (let ?p = 1 in ((\ () -> ?p + 1) :: (() -> ((?p :: Int) => Int)))) ()
2
Prelude> let ?p = 5 in (((let ?p = 1 in \ () -> ?p + 1) :: (() -> ((?p :: Int) => Int)))) ()
6

As far as I can tell, we need to tell the type-checker about the higher-rank as close to the desired location as possible in order to see this behavior.

[simonpj]

I've tidied this up I think. It's all rater a dark corner. GHC now treat types

   type1 -> (context) => type2
   (context) => type1 -> type2

essentially identically.

Simon