Instance chaining seems to fail

[jackfirth]

The following program fails to typecheck:

#lang hackett

(class (Base a)
  [base : {a -> a -> a -> a}])

(class (Middle a)
  [middle : {a -> a -> a}])

(class (Top a)
  [top : {a -> a}])

(instance (∀ [a] (Middle a) => (Base a))
          [base (λ [_] middle)])

(instance (∀ [a] (Top a) => (Middle a))
          [middle (λ [_] top)])

The type checker throws the error typechecker: could not deduce (Top a18) in: (case* (_27) ((_) middle)) with (λ [_] middle) as the error's source location. I think this is supposed to work, since this equivalent Haskell program typechecks successfully:

class Base a where
  base : a -> a -> a -> a

class Middle a where
  middle : a -> a -> a

class Top a where
  top : a -> a -> a

instance Middle a => Base a where
  base _ = middle

instance Top a => Middle a where
  middle _ = top

[lexi-lambda]

I haven’t looked into this, but my guess is that the issue is there are two instances in scope, the local one from the Base a instance constraint and the global one from the Middle a instance declaration. Both instances match, but Hackett appears to currently be picking the global one, which means it attempts to solve the Top a subgoal. I think it should prefer the one from the constraint, since it doesn’t have any subgoals.