agda2hs icon indicating copy to clipboard operation
agda2hs copied to clipboard

Support using instances from applied modules in canonicity check

Open jespercockx opened this issue 11 months ago • 0 comments

This is the remaining issue with parametrized modules after the merging of https://github.com/agda/agda2hs/pull/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 avatar Mar 22 '24 16:03 jespercockx