Support using instances from applied modules in canonicity check

[jespercockx]

This is the remaining issue with parametrized modules after the merging of #307:

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 message:

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

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. However, I do not know of any way to reconstruct this instance table.

[jespercockx]

This issue is no longer there for the new canonicity check.