Bug in type class treatment?

[mgree]

It seems like Lem doesn't let typeclass instances use generic helpers on that typeclass. It's a thing I expect to work in, e.g., Haskell.

As a minimal example, consider the following code, in a file bug.lem.

open import Pervasives

class ( Bug 'a )
  val one : 'a -> nat
  val two : 'a -> nat
end

val ext : forall 'a. Bug 'a => 'a -> nat
let ext v = one v + 1

instance (Bug nat)
  let one n = n
  let two n = ext n
end

When I run lem bug.lem, I get the following error message:

File "bug.lem", line 13, character 3 to line 13, character 19
  Type error: unsatisfied type class constraint:
    (Bug.Bug nat)

I define a typeclass Bug 'a with one, two : 'a -> nat. Before defining an instance, I define a helper function ext that should work for any Bug instance. I then try to use that helper in an instance definition, but it seems that the Lem type system doesn't believe that a current instance exists yet.

P.S. Sorry for duplication---I posted an issue to bitbucket before realizing you'd moved here.