Opened 3 years ago
Closed 5 months 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 Revisions: |
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 3 years ago by simonpj
- Priority changed from normal to high
comment:2 Changed 3 years ago by simonpj
- Test Case changed from indexed-types/should_fail/T4272 to indexed-types/should_fail/T5763
comment:3 Changed 3 years ago by simonpj
- Owner set to simonpj
comment:4 Changed 3 years ago by igloo
- Milestone changed from 7.6.1 to 7.6.2
comment:5 Changed 2 years ago by liyang
- Cc hackage.haskell.org@… added
comment:6 Changed 21 months ago by wira
can i know too problem solving
comment:7 Changed 9 months ago by thoughtpolice
- Priority changed from high to normal
Lowering priority (these tickets are assigned to older versions, so they're getting bumped as they've been around for a while).
comment:8 Changed 9 months ago by thoughtpolice
- Milestone changed from 7.6.2 to 7.10.1
Moving to 7.10.1.
comment:9 Changed 5 months ago by thomie
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 5 months ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case indexed-types/should_fail/T5763 deleted
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.