Infinite loop while resolving instances

[AlexKnauth]

Running a program where deriving instances produces a cycle gets into an infinite loop.
Here the (C (List Integer)) instance produces the subgoal (C (Tuple Integer (List Integer))), which produces the subgoals (C Integer) and (C (List Integer)). It doesn't recognize that the (C (List Integer)) subgoal is what it was originally trying to solve, and stop the loop.

As an aside, the vanilla Haskell version of this errors saying

• Non type-variable argument in the constraint: C (a, [a])
(Use FlexibleContexts to permit this)

Unless I use both FlexibleContexts and UndecidableInstances.

There are several ways Hackett could "fix" this.
(1) By disallowing non-type-variable arguments in constraints, like Haskell does without FlexibleContexts.
(2) By recognizing the cycle and erroring, like Haskell does with FlexibleContexts but without UndecidableInstances.
(3) By letting it through somehow, like Haskell does with both FlexibleContexts and UndecidableInstances.

But it should not both let the ∀ [a] (C (Tuple a (List a))) => (C (List a)) instance through and loop when it tries to use it.

#lang hackett

(class (C a)
  [c : {a -> Integer}])

(instance (C Integer) [c id])
(instance (∀ [a b] (C a) (C b) => (C (Tuple a b)))
  [c (λ* [[(Tuple a b)] {(c a) + (c b)}])])

(instance (∀ [a] (C (Tuple a (List a))) => (C (List a)))  ; this "goes through" fine
  [c (λ* [[Nil] 0]
         [[{fst :: rst}] (c (Tuple fst rst))])])

(c (List 1 2 3 4))  ; this causes the infinite loop

[iitalics]

Does Haskell get in a loop when you do this and use UndecidableInstances? My understanding was that UndecidableInstances should allow you to do stuff like this at your own risk. Hackett's instance resolver is naive but probably gives you this same amount of (unchecked) power.

[AlexKnauth]

No, with FlexibleContexts and UndecidableInstances it succeeds and (c [1, 2, 3, 4]) returns 10.

[lexi-lambda]

Yes, this is tricky. I probably won’t have time to look into this until after Curry On, but this is a good report. It seems like GHC does some knot-tying here that Hackett ought to do as well.