Pattern matching allows you to turn (x y : A) -> A into (@0 x y : A) -> A

[Saizan]

postulate
  A : Set

open import Agda.Builtin.Equality

foo : (f : A → A → A) (@0 g : @0 A → @0 A → A)
    → @0 _≡_ {A = @0 A → @0 A → A} g (\ x y → f y x)
    → @0 A → @0 A → A
foo f g refl = g
  -- In the goal, `C-c C-n g` gives
  -- λ (@0 x) (@0 y) → f y x
  -- which is only well-typed in an erased context.

bad : (f : A → A → A) → @0 A → @0 A → A
bad f = foo f (\ x y → f y x) refl

[jespercockx]

Debug output from the unifier:

initial unifyState: UnifyState
                      variable tel:   (f : A → A → A) (@0 g : @0 A → @0 A → A)
                      flexible vars:  [(1,NotForced),(0,NotForced)]
                      equation tel:   (_ : @0 A → @0 A → A)
                      equations:      g =?= λ (@0 x) (@0 y) → f y x
isEtaVar results:  [Just 0,Nothing]
trying unifyStep Solution
                   position:    0
                   type:        @0 A → @0 A → A
                   variable:    (0,Just 0,NotForced,ImplicitFlex)
                   term:        λ (@0 x) (@0 y) → f y x
forcedVars = []
u          = λ (@0 x) (@0 y) → @3 y x
p          = .(λ (@0 x) (@0 y) → @3 y x)
bound      = []
dotSub     = idS
Equation type:  @0 A → @0 A → A
Variable type:  @0 A → @0 A → A
Modality ok:  True
unifyStep successful.
new unifyState: UnifyState
                  variable tel:   (f : A → A → A)
                  flexible vars:  [(0,NotForced)]
                  equation tel:  
                  equations:     

It seems that somehow the x and y in the lambda expression got annotated with @0, producing the ill-typed term λ (@0 x) (@0 y) → f y x. So something already went wrong before we got to this point.

[jespercockx]

Please ignore my previous comment, I completely missed the point that λ (@0 x) (@0 y) → f y x is well-typed as long as we're in an erased context. So the problem is that by unification we moved something from an erased to a non-erased context.

[Saizan]

The term λ (@0 x) (@0 y) → f y x is the one from the type, and it is fine there because it's an erased context.

I'm looking into keeping track of the Modality in AsBinding, it might solve the issue, because really I shouldn't be allowed to use g in the body of foo.

[jespercockx]

That seems like a good thing to do. In the clause the variable g is really an as pattern g@.(λ (@0 x) (@0 y) → f y x), which is threated as a let binding so it should use the modality of the body of the let. In general all dot patterns come directly from the type of the function, i.e. from an erased context, so a conservative approach would be to mark all dot patterns as being erased. However that would probably cause quite some breakage. A more backwards-compatible solution would be to analyze the term in the dot pattern and see if it is usable at non-erased modality.

[Saizan]

With 8eeb1f6 Agda will complain that g is erased and cannot be used in the body of foo.

We can still define bar below though

bar : (f : A → A → A) (g : @0 A → @0 A → A)
    → @0 _≡_ {A = @0 A → @0 A → A} g (\ x y → f y x)
    → @0 A → @0 A → A
bar f g refl = g

I couldn't find a way to break erasure with bar, but it seems iffy to have clause that essenntially says bar f _ refl = \ (@0 x y) -> f y x because that exact body wouldn't typecheck. I think making usableMod care about bound variables will fix this.

[Saizan]

I keep seeing your replies only after I post something :)

Wherever we were producing an AsBinding we had a whole Dom Type rather than a Type, so I just used the Modality from the Dom. it should match up with the modality the particular function argument is declared with, right? Hopefully it's propagated correctly for nested patterns.