Fix for issue #305 + some related problems

[jespercockx]

This fixes #305 by setting the right checkpoint for Agda so that when we call instance search for checking canonicity, the instances are correctly applied to the module parameters.

I also found and fixed a related regression introduced in my PR #304 that caused us to no longer check the canonicity of superclass instances when defining a subclass instance.

When I run the test suite locally on this branch, there is something weird that happens with the golden files for two modules:

• NonCanonicalSuperclass.agda produces an unexpected success despite producing the correct error when running agda2hs on it directly
• StreamFusion.agda I did not touch in any way, but suddenly appears in a different location

I feel like our test suite is getting increasingly flaky and hard to manage, so perhaps we should look into improving it soon (#153)

[omelkonian]

StreamFusion.agda I did not touch in any way, but suddenly appears in a different location

c.f. the changes of 416234a, where I moved the cubical tests under Cubical for a more consistent test folder structure

[jespercockx]

c.f. the changes of 416234a, where I moved the cubical tests under Cubical for a more consistent test folder structure

I get that you changed it, but I don't understand why StreamFusion.hs still appears in the golden directory rather than in golden/Cubical.

Also there apparently are internal errors here in CI that do not show up when I run the tests locally. Mysterious... Perhaps it's picking up the wrong version of agda2hs somehow?

[jespercockx]

I think that was it: after manually deleting test/agda2hs the discrepancies suddenly went away. Though now there are still CI errors that I cannot produce locally. The mystery hunt continues!

[jespercockx]

After exorcising the ghosts from my repository I managed to fix the remaining internal errors over the weekend. However, the issue still remains when a class function is used inside a pattern-matching lambda:

module _ (@0 X : Set) where

record Class (a : Set) : Set where
  field
    foo : a → a
open Class {{...}} public

{-# COMPILE AGDA2HS Class class #-}

instance
  ClassInt : Class Int
  ClassInt .foo = _+ 1

{-# COMPILE AGDA2HS ClassInt #-}

yetAnotherTest : Int
yetAnotherTest = case Just True of λ where
  Nothing → error "unreachable"
  (Just y) → foo 5
{-# COMPILE AGDA2HS yetAnotherTest #-}

still gives the error:

No instance of type Class Int was found in scope.

[jespercockx]

I got one step further again: the checkpoint is now being set in the context of the module rather than the context of an individual clause, which means the example above now works. However, the problems are still not over as the check still fails when the instance is defined in a different module that is applied and opened in the current module:

record Class (a : Set) : Set where
  field
    foo : a → a
open Class {{...}} public
{-# COMPILE AGDA2HS Class class #-}

module M1 (@0 X : Set) where

  instance
    ClassInt : Class Int
    ClassInt .foo = _+ 1
  {-# COMPILE AGDA2HS ClassInt #-}

module M2 (@0 X : Set) where

  open M1 X

  tester : Int
  tester = foo 41
  {-# COMPILE AGDA2HS tester #-}

Error is the same as before:

No instance of type M1.Class X Int was found in scope.

I guess the problem is that we are using the instance table of the top-level module rather than the one that was used inside the module M2, and this top-level instance table does not include the instances from locally opened modules.

[omelkonian]

Let's see if we can use Origin::UserWritten to only run the consistency check in these cases, thus allowing us not to re-typecheck and re-construct everything that Agda has done before.

[jespercockx]

Here is a real-world example that triggered this error: https://github.com/jespercockx/agda-core/blob/20a4eac77466560730b5243faeed306a5aa98cf8/src/Agda/Core/Typechecker.agda#L41-L42

Here the call to return from the Monad typeclass causes the check to fail, because the instance for Monad TCM is defined in a different module.

[jespercockx]

Let's see if we can use Origin::UserWritten to only run the consistency check in these cases, thus allowing us not to re-typecheck and re-construct everything that Agda has done before.

Unfortunately this does not work: in Agda's internal syntax, calls to type class functions are represented as a Proj elimination, which does not include any ArgInfo with the Origin. It does have a ProjOrigin, but this seems to be set to ProjPrefix whether or not the instance was written by hand so it is useless for our purpose here. So unfortunately it seems we do not have the information available to determine whether the argument was provided manually or not.

(As an aside: Agda's pretty-printer seems to struggle with a similar problem, as it prints foo 41 here as Class.foo ClassInt (int64 41).)

[jespercockx]

Since this PR constitutes a clear improvement to the status quo and I don't have a solution for the remaining problem, I believe it's best to merge this now and leave adding support for using instances coming from module applications as a separate issue.