#5763: Confusing error message
---------------------------------+------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 7.6.1
Component: Compiler | Version: 7.2.2
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase: indexed-types/should_fail/T4272
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
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.)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5763>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
