[Agda] Instance Search fails with parameterized modules?

[Joey Eremondi]

Perfect, I didn't realize it was a "too many candidates" problem, I just
thought it was stuck on unsolved metas.
Thanks!

On Wed, Nov 27, 2019 at 11:48 PM Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/301cc7e4/attachment.html>