Error `[no locals in scope]` for interface constants on Equality.

[fabianhjr]

Steps to Reproduce

module Test

interface TMonoid a where
  op : a -> a -> a
  e : a

interface TMonoid a => TGroup a where
  inv : a -> a
  proofOfLeftInverse  : (x : a) -> (inv x) `op` x = e
  proofOfRightInverse : (x : a) -> x `op` (inv x) = e

Expected Behavior

To type-check

Observed Behavior

Test.idr:9:53--10:3:While processing type of proofOfLeftInverse at Test.idr:9:3--10:3:
Can't solve constraint between:
    ?type_of_e [no locals in scope]
and
    a

[ziman]

It seems e is bound as a free implicit. If you say Test.e instead, the file typechecks.