[Agda] Instance Search fails with parameterized modules?

[Joey Eremondi]

I'm hitting errors I don't understand with instance search, and I've boiled
it down to a (fairly) minimal example:

module Minimal where

open import Relation.Binary.PropositionalEquality

open import Agda.Primitive

module A where
record ToDyn {l} (TheDyn : Set l) (a : Set l) : Set l where
field
toDyn : a -> TheDyn
fromDyn : TheDyn -> a

open ToDyn {{...}} public


module B (DynB : ∀ (l) -> Set l) where

open A
record GType (l) : Set (lsuc l) where
field
~_ : Set l
{{dynInst}} : ToDyn (DynB l) ~_

open GType public

toG : ∀ {l} -> (t : Set l) -> {{dinst : ToDyn (DynB l) t}} -> GType l
toG t {{dinst}} = record {~_ = t ; dynInst = dinst}


module C (DynC : ∀ (l) -> Set l) where
open A
open B DynC

record GPi {l1 l2} (dom : GType l1) (cod : ~ dom -> GType l2) : Set (l1 ⊔
l2) where
field
apply : (x : ~ dom) -> ~ (cod x)

setPi : ∀ {l1 l2} -> (dom : Set l1) -> (cod : ( dom) -> Set l2) ->
{{ idom2 : ToDyn (DynC l1) dom}} -> {{ icod2 : {x : dom} -> ToDyn (DynC l2)
(cod x)}} -> Set (l1 ⊔ l2)
setPi {l1} {l2} dom cod {{idom2}} {{icod2}} = GPi (toG dom ) λ x → toG (cod
x)



module D (DynD : ∀ (l) -> Set l) where
open A
open B DynD
open C DynD

data Nat : Set where
NZ : Nat
NS : Nat -> Nat

instance
unwrapDynInst : ∀ {l} { a : GType l} -> ToDyn (DynD l) (~ a)
unwrapDynInst {l} {record { ~_ = ~_ ; dynInst = dynInst }} = dynInst

someFun : {{_ : ToDyn (DynD lzero) Nat}} -> setPi Nat (\ _ -> Nat)
someFun = {!!}



I've got four modules:
* Module A defines a record (i.e. typeclass) with some functions
* Module B defines an existential type along with the class from module A
* Module C defines Pi types over these existential types
* Module D tries to construct a function of this Pi type

You can run the code yourself, but on Agda 2.6.0.1 I get the following
error:

Failed to solve the following constraints:
Resolve instance argument
_icod2_66
: (DynD₁ : (l : Level) → Set l) ⦃ _ = z : ToDyn (DynD₁ lzero) Nat ⦄
{x : Nat} →
ToDyn (DynD₁ lzero) Nat
Candidates
DynD : ToDyn (@2 lzero) Nat
λ {l} → unwrapDynInst :
{l : Level} {a : GType l} → ToDyn (@4 l) (~ a)
Resolve instance argument
_idom2_65
: (DynD₁ : (l : Level) → Set l)
⦃ _ = z : ToDyn (DynD₁ lzero) Nat ⦄ →
ToDyn (DynD₁ lzero) Nat
Candidates
_ : ToDyn (DynD lzero) Nat
λ {l} → unwrapDynInst :
{l : Level} {a : GType l} → ToDyn (DynD l) (~ a)


And here's my confusion: it's looking for ToDyn (DynD₁ lzero) Nat and it
has a candidate ToDyn (DynD lzero) Nat.

So, what is the subscript 1 on DynD? Why does it think there are two
different versions of DynD, that it doesn't unify? Is this a bug, or
behaviour I just don't understand? And is there a way to work around this
without manually writing the instances everywhere (which defeats the point
of instance arguments)?

Thanks!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191127/0473a15c/attachment.html>