Opened 5 years ago
Closed 2 years ago
#5763 closed bug (fixed)
Confusing error message
Reported by: | simonpj | Owned by: | simonpj |
---|---|---|---|
Priority: | normal | Milestone: | 7.10.1 |
Component: | Compiler | Version: | 7.2.2 |
Keywords: | Cc: | dimitris@…, hackage.haskell.org@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
For test indexed-types/should_fail/T4272
we get this type error
T4272.hs:11:16: Occurs check: cannot construct the infinite type: x0 = TermFamily x0 x0 Expected type: TermFamily x0 x0 Actual type: TermFamily a a In the first argument of `prune', namely `t' In the expression: prune t (terms (undefined :: TermFamily a a)) In an equation for `laws': laws t = prune t (terms (undefined :: TermFamily a a))
It's not at all obvious why unifying (TermFamily x0 x0)
with (TermFamily a a)
should yield an occurs check. Especially as TermFamily
is a type function with arity 1, and x0
is a unification variable. So the natural way to solve this constraint would be to unify x0
with a
, and then the constraint is satisfied.
What goes wrong is that there is another insolube constraint (which is also reported):
T4272.hs:11:19: Could not deduce (a ~ TermFamily x0 x0) from the context (TermLike a) bound by the type signature for laws :: TermLike a => TermFamily a a -> b at T4272.hs:11:1-54 `a' is a rigid type variable bound by the type signature for laws :: TermLike a => TermFamily a a -> b at T4272.hs:11:1 In the return type of a call of `terms' In the second argument of `prune', namely `(terms (undefined :: TermFamily a a))' In the expression: prune t (terms (undefined :: TermFamily a a))
The constraint solver finds this latter constraint, can't solve it, but still uses it to simplify the first one, by substituting (TermFamily x0 x0)
for a
; and that is what gives the occurs check error.
I don't think that we should use insoluble constraints to rewrite unsolved constraints. But it's delicate, so I am not trying to fiddle right now. Hence making this ticket.
(Incidentally, it's not a regression; it's been like this forever.)
Change History (10)
comment:1 Changed 5 years ago by
Priority: | normal → high |
---|
comment:2 Changed 5 years ago by
Test Case: | indexed-types/should_fail/T4272 → indexed-types/should_fail/T5763 |
---|
comment:3 Changed 5 years ago by
Owner: | set to simonpj |
---|
comment:4 Changed 5 years ago by
Milestone: | 7.6.1 → 7.6.2 |
---|
comment:5 Changed 4 years ago by
Cc: | hackage.haskell.org@… added |
---|
comment:7 Changed 3 years ago by
Priority: | high → normal |
---|
Lowering priority (these tickets are assigned to older versions, so they're getting bumped as they've been around for a while).
comment:9 Changed 2 years ago by
Is this problem solved?
T4272
doesn't show the Occurs check
message anymore (as also noted by SPJ in da71a9524ffff0865222127bef09fd04a1359a53), but maybe this is incidental? I can not find test T5763
anywhere, so I'll leave this open for now.
Output of running the command "git show 0b3c3c81792c88ee40687f86bed4935e721dabe0 testsuite/tests/indexed-types/should_fail/T4272.stderr":
Author: Dimitrios.Vytiniotis <> Date: Wed Apr 4 14:41:11 2012 +0100 Error message modifications following ghc-new-solver modifications diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr index 24f0cbd..e809d9c 100644 --- a/testsuite/tests/indexed-types/should_fail/T4272.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr @@ -1,29 +1,6 @@ -T4272.hs:11:16: - Couldn't match type `TermFamily (TermFamily x0 x0)' - with `TermFamily x0' - NB: `TermFamily' is a type function, and may not be injective - The type variable `x0' is ambiguous - Possible fix: add a type signature that fixes these type variable(s) - Expected type: TermFamily x0 x0 - Actual type: TermFamily a a - In the first argument of `prune', namely `t' - In the expression: prune t (terms (undefined :: TermFamily a a)) - In an equation for `laws': - laws t = prune t (terms (undefined :: TermFamily a a)) - -T4272.hs:11:16: - Occurs check: cannot construct the infinite type: - x0 = TermFamily x0 x0 - Expected type: TermFamily x0 x0 - Actual type: TermFamily a a - In the first argument of `prune', namely `t' - In the expression: prune t (terms (undefined :: TermFamily a a)) - In an equation for `laws': - laws t = prune t (terms (undefined :: TermFamily a a)) - -T4272.hs:11:19: - Could not deduce (a ~ TermFamily x0 x0) +T4272.hs:11:26: + Could not deduce (a ~ TermFamily a a) from the context (TermLike a) bound by the type signature for laws :: TermLike a => TermFamily a a -> b @@ -31,7 +8,10 @@ T4272.hs:11:19: `a' is a rigid type variable bound by the type signature for laws :: TermLike a => TermFamily a a -> b at T4272.hs:10:16 - In the return type of a call of `terms' + Expected type: TermFamily a (TermFamily a a) + Actual type: TermFamily a a + In the first argument of `terms', namely + `(undefined :: TermFamily a a)' In the second argument of `prune', namely `(terms (undefined :: TermFamily a a))' In the expression: prune t (terms (undefined :: TermFamily a a))
comment:10 Changed 2 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | indexed-types/should_fail/T5763 |
Well we indeed no longer use insoluble constraints to rewrite others, so yes, I think we can close this.
Simon
I'll make it high priority to make sure I look at it for 7.6. But it's not really that serious.