Opened 10 months ago

Last modified 9 months ago

#15888 new bug

Quantified constraints can be loopy

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.6.2
Keywords: QuantifiedConstraints Cc:
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

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:

  1. We get a Wanted C (T1 Int).
  1. GHC chooses the appropriate instance, emitting a Wanted forall a. C (T2 a).
  1. GHC skolemizes the a to a1 and tries solve a Wanted C (T2 a1).
  1. GHC chooses the appropriate instance, emitting a Wanted forall a. C (T1 a).
  1. GHC skolemizes the a to a2 and tries to solve a Wanted C (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.

Change History (1)

comment:1 Changed 9 months ago by bgamari

Milestone: 8.6.3

Ticket retargeted after milestone closed

Note: See TracTickets for help on using tickets.