Print non-identity module parameter substitution? (with on variable)

[GoogleCodeExporter]

open import Common.Prelude
open import Common.Equality

id : (A : Set) → A → A
id A x = x

f : Bool → Bool
f x = true where

  z : Bool → Bool
  z true = x
  z false = x

  y : ∀ q → x ≡ z q
  y with x
  y | true   = id {!!} λ { true → refl ; false → refl }
  y | false  = id {!!} λ { true → refl ; false → refl }

Agda solves these meta-variables (C-c C-=) but does not accept the solution
(C-c C-s).

?0 := (q : Bool) → true ≡ z q
?1 := (q : Bool) → false ≡ z q

Original issue reported on code.google.com by andreas....@gmail.com on 5 Nov 2014 at 8:38

[GoogleCodeExporter]

A reduced example:

open import Common.Equality

data Unit : Set where
  unit : Unit

id : (A : Set) → A → A
id A a = a

module _ (x : Unit) where

  dx : Unit → Unit
  dx unit = x

  g : ∀ u → x ≡ dx u
  g with x
  g | unit  = id {!((u : Unit) → unit ≡ dx u)!} ?

Original comment by andreas....@gmail.com on 6 Nov 2014 at 6:50

• Added labels: Modules, With
• Removed labels: ExtendedLambda

[GoogleCodeExporter]

It is very difficult to understand what is going on here, as Agda censors the arguments coming from a module telescope (the "free variables"). However, in this case, one variable becomes non-free, the "x". Let us manually expand away the module parameter (x : Unit):

  dx : (x : Unit) → Unit → Unit
  dx x unit = x

  g : (x : Unit) → ∀ u → x ≡ dx x u
  g x with x
  g x | unit  = id ((u : Unit) → unit ≡ dx x u) ?

As "dx" is a definition, it is always applied to the free variables of the current module, here, x. However, due to "with", the variable gets replaced by unit in the type of g. In the with-clause, we are at type

  forall u -> unit == dx unit u

In the user written expression (and the one generated by Agda from the solved constraint), dx is automatically applied to the free variable dx.

Oops!

We lose information when printing terms and parsing them back, even if we print all implicit arguments. Because arguments coming from a module telescope are always censored away, even to the poor Agda developer trying to debug.

Seems that not only I do not understand the "section free vars", but also the original developer... :-E>

Original comment by andreas....@gmail.com on 6 Nov 2014 at 8:34

• Changed state: Started

[GoogleCodeExporter]

The question is how to solve this dilemma. For one, if a free variable ever gets "non-free", i.e., replace by another term, Agda should crash. So we can find all the bugs.

Secondly, we need to see where free variables can get captured and forbid this. This would mean that you cannot 'with' on a pattern variable. It is anyway a stupid thing to do, just pattern match!

Original comment by andreas....@gmail.com on 6 Nov 2014 at 8:41

[GoogleCodeExporter]

For now, I fixed this by disallowing with on a module parameter. One could be a bit more friendly and just disallow such a with if it actually abstracts a module parameter in a type, or silently not abstract over this module parameter. My criterion is simple to comprehend. And not backwards-compatible, of course.

Fix: e2cf1f5
CHANGELOG: 2f0ee51

Original comment by andreas....@gmail.com on 6 Nov 2014 at 11:35

• Changed state: Fixed
• Removed labels: Conversion, Meta

[andreasabel]

Since we can refine module parameters now officially, we could allow with on a module parameter. However, since we throw away the module parameter instantiation in printing, the incomprehensible error would stay.
We first need to find a way to print non-identity module parameter substitutions to the user.

[UlfNorell]

Example where you don't with on a variable:

open import Agda.Builtin.Nat

postulate
  f : Nat → Nat

data D : Nat → Set where
  d : ∀ n → D (f n)


module _ (n : Nat) where

  postulate
    h  : Nat
    dh : D h

  g : D n → D h
  g (d m) with f m
  ... | z = dh -- error z != f m

[andreasabel]

@Saizan : Can you extend the substitution printing to the parameter dropping case? I.e. only silently drop parameter arguments to a defined symbol if they are identical to the original parameters (i.e. the correct de Bruijn index). Otherwise, they are printed in substitution notation.
Then we could allow with on variables again and close this issue.

[UlfNorell]

if they are identical to the original parameters (i.e. the correct de Bruijn index)

This is not the correct criterion though. They should be printed if they differ from the parameters that get filled in, and these may have been refined. Those are computed by freeVarsToApply.

[Saizan]

This is not the correct criterion though. They should be printed if they differ from the parameters that get filled in, and these may have been refined. Those are computed by freeVarsToApply.

freeVarsToApply will give me the correct arguments to compare with (I guess?), but
currently I drop the substitution only if both sides are variables, in fact we get the following behavior for metas

module M0 (n : Nat) where

  bar : ∀ m →  Σ Nat \ x → n ≡ suc m → x ≡ zero
  bar m = { }0 , \ { refl → { }1 }

  -- ?1 : ?0 (n = (suc m)) ≡ zero

Which actually seems reasonable to me here, but maybe we disagree here?

If we put the refinement outside the sigma we get no substitution simply because the meta won't have n as a free var from the start.

  foo : ∀ m → n ≡ suc m → Σ Nat \ x → x ≡ zero
  foo m refl = { }2 , { }3
  
  --  ?3 : ?2 ≡ zero

What's an example with defined symbols and refinement that I should keep in mind?

[UlfNorell]

Here's a simple one

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

module _ (n : Nat) where

  postulate Goal : Set

  foo : n ≡ 0 → Goal
  foo refl = {!!} -- Goal  or  Goal (n = 0)

The argument for printing the goal as Goal without the substitution is that this is exactly the substitution that gets filled in when you just write Goal at that point.

On the other hand, if you do

  bar : Goal
  bar with n
  ... | m = {!!}  -- should be: Goal (n = m)

you need to print the substitution since Goal by itself would get filled in with Goal (n = n). This is the reason for with-on-module-parameter being disabled at the moment.

[Saizan]

Is checkSyntacticEquality a good choice to compare these arguments? using conversion would require to infer the types.

[Saizan]

@andreasabel I have implemented something that seems reasonable to me, but it seems to have issues when printing termination problems, you can try running make fail from this branch:

Saizan@501a7fa

[UlfNorell]

Most likely the same problem as #3136.

[andreasabel]

Should we go ahead with this issue and allow with on module parameters now?

[UlfNorell]

I don't see why not.

[jespercockx]

I talked with Andreas about this over lunch but I'm a bit hesitant. Currently there's an invariant that at any point inside a parametrized module, all definitions in the module are applied to the same (possibly refined) terms for the parameters. This invariant would be broken if we allow case splitting on module parameters. I know at least the logic for rewrite rules inside parametrized modules actually relies on this invariant.