[Agda] mutual strangeness

[Dan Licata]

Hi everyone,

I've noticed this too, as well as a few other curious behaviors:


1) The order of declarations in a mutual block matters; e.g.

  mutual 
    data Foo : Set where
      F : Foo

    data Bar : Foo2 -> Set where
      B : Bar F

    Foo2 : Set
    Foo2 = Foo

is not accepted (because Foo2 is not in scope in Bar's type)
but moving Foo2's declaration above Bar's fixes the problem.


2) The order of declarations influences which definitions are expanded:

  mutual 
    data Foo : Set where
      F : Foo

    Foo3 : Set
    Foo3 = Foo2

    data Bar : Foo3 -> Set where
      B : Bar F

    Foo2 : Set
    Foo2 = Foo

is well-scoped, but doesn't type check, because Foo !=< Foo2 (but moving
the definition of Foo2 above Bar fixes the problem).


Are there reasons for these restrictions, or are they just artifacts of
the implementation?

-Dan

On Jan31, Thorsten Altenkirch wrote:
> Hi,
> 
> it seems that constructors are not visible in the types of mutually  
> defined functions. This is especially strange since one can just  
> define an auxilliary function to overcome this restriction.
> 
> E.g. having another go at a total syntax of type theory I tried:
> 
> >module tt0 where
> >
> >mutual
> >
> >  data Con : Set where
> >    empty : Con
> >    _*_ : (Γ : Con) → Ty Γ → Con
> >
> >  data Ty : Con → Set where
> >
> >  data Tms : Con → Con → Set where
> >
> >  wkSubst : ∀ {Γ} → (σ : Ty Γ) → Tms (Γ * σ) Γ
> >  wkSubst {Γ} σ = ?
> 
> and the scoper complaints:
> 
> >Not in scope:
> >  * at /Users/txa/Drafts/setoids/tt0.agda:13,41-42
> >when scope checking Γ * σ
> 
> However, it is easy to overcome this by
> 
> >module tt1 where
> >
> >mutual
> >
> >  data Con : Set where
> >    empty : Con
> >    _*_ : (Γ : Con) → Ty Γ → Con
> >
> >  data Ty : Con → Set where
> >
> >  data Tms : Con → Con → Set where
> >
> >  _**_ : (Γ : Con) → Ty Γ → Con
> >  Γ ** σ = Γ * σ
> >
> >  wkSubst : ∀ {Γ} → (σ : Ty Γ) → Tms (Γ ** σ) Γ
> >  wkSubst {Γ} σ = {! !}
> 
> which is accepted. Hence, wouldn't it make more sense to get rid of  
> this restriction alltogether?
> 

> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda