[Agda] Instance Search fails with parameterized modules?

[Ulf Norell]

The subscript is to avoid shadowing the module parameter DynD.

The problem here is that there are multiple possible candidates for the
instance goals. In the first case both DynD and unwrapDynInst are possible,
and in the second case both the unnamed ToDyn argument and unwrapDynInst.

If you don't make unwrapDynInst `instance` it works.

/ Ulf

On Thu, Nov 28, 2019 at 7:06 AM Joey Eremondi <joey.eremondi at gmail.com>
wrote:

> 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!
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191128/c9484b23/attachment.html>