Quantified constraints can be loopy
Consider this abuse:
{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
module Bug where
data T1 a
data T2 a
class C a where
meth :: a
instance (forall a. C (T2 a)) => C (T1 b) where
meth = error "instance T1"
instance (forall a. C (T1 a)) => C (T2 b) where
meth = error "instance T2"
example :: T1 Int
example = meth
GHC says
• Reduction stack overflow; size = 201
When simplifying the following type: C (T1 a)
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: meth
In an equation for ‘example’: example = meth
Of course, I've taken on some responsibility for my actions here by saying UndecidableInstances
, but GHC really should be able to figure this out. Here's what's happening:
- We get a Wanted
C (T1 Int)
. - GHC chooses the appropriate instance, emitting a Wanted
forall a. C (T2 a)
. - GHC skolemizes the
a
toa1
and tries solve a WantedC (T2 a1)
. - GHC chooses the appropriate instance, emitting a Wanted
forall a. C (T1 a)
. - GHC skolemizes the
a
toa2
and tries to solve a WantedC (T1 a2)
.
And around and around we go.
(This loop is guessed at from knowing GHC's algorithms in general. I did not look at a trace.)
We could get this one, though. Before skolemizing, we could stash the Wanted in the inert_solved_dicts
, which is where we record uses of top-level instances. (See Note [Solved dictionaries]
in TcSMonad.) Then, later, when we see the same Wanted arise again, we would just use the cached value, making a well-formed recursive dictionary.
This deficiency was discovered in singletons
(https://github.com/goldfirere/singletons/issues/371). Perhaps that's not "the wild", but it's not quite contrived either.
Note that we don't need two datatypes to trigger this, but having one recursive instance like this seems awfully silly.
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |