agda2hs
agda2hs copied to clipboard
Support using instances from applied modules in canonicity check
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.