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 |