Lifting constraints is questionably correct for implicit parameters.

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). :)

Trac metadata

Trac field	Value
Version	6.12.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture