Overzealous pruning (reprise)

[vlopezj]

Previously: #458, #1153.

Agda throws away solutions when pruning arguments containing variables of record Unit type.
Here are some examples.

module Prune where

record Unit : Set where
  constructor tt
  
postulate F : Set → Set 
postulate a : Set → Unit → Set

postulate kA : {M : Set → Set → Set} → 
               ((x : Set) (y : Unit) → F (M x (a x y))) → 
               Set


postulate kB : {M : Set → Set → Set} → 
              ((x : Set) (y : Unit) → F (M x (a x y))) → 
              ((x : Set) (y : Set) → F (M x y)) → 
              Set

postulate F' : (A : Set) → F A

-- Some problems
-- ?M : Set → Set → Set

---------------------------------
K1 : Set
K1 = kA (\x y → F' (a x tt))
---------------------------------
-- Unification problem: ∀(x:Set)(y:Unit). ?M x (a x y) ≈ a x tt
-- Agda solution:       ?M := \ x _ → a x tt 
-- Expected:            No solution, because (?M := \ _ b → b is also a solution)
---------------------------------

---------------------------------
K2 : Set
K2 = kB (\x y → F' (a x tt))
        (\x y → F' (a x tt))
---------------------------------
-- Unification problem:  ∀(x:Set)(y:Unit). ?M x (a x y) ≈ a x tt
--                     ∧ ∀(x:Set)(y:Set).  ?M x y       ≈ a x tt
-- Agda solution:        ?M := \x _ → a x tt
-- Expected solution:       [idem.]
--------------------------------

--------------------------------
K3 : Set
K3 = kB {\x y → y}
        (\x y → F' (a x tt))
        (\x y → F' y)
--------------------------------
-- Unification problem:  ∀(x:Set)(y:Unit). (\x y → y) x (a x y) ≈ a x tt
--                     ∧ ∀(x:Set)(y:Set).  (\x y → y) x y       ≈ y
-- Agda solution:        OK
-- Expected solution:    OK
--------------------------------

--------------------------------
K4 : Set
K4 = kB (\x y → F' (a x tt))
        (\x y → F' y)
--------------------------------
-- Unification problem:   ∀(x:Set)(y:Unit). ?M x (a x y) ≈ a x tt
--                      ∧ ∀(x:Set)(y:Set).  ?M x y       ≈ y
-- Agda solution:        ERROR (y ≠ a x tt : Set)
-- Expected solution:    ?M := \x y → y   (cf. `K3`)
--------------------------------

Tested with Agda version 2.6.0-c284008. Here is the offending function:

agda/src/full/Agda/TypeChecking/MetaVars/Occurs.hs

Line 528 in c284008

hasBadRigid :: [Nat] -> Term -> ExceptT () TCM Bool

I think that the behaviour of Agda when typechecking K1, and specially K4 is a bug. The problem is that the meta argument a x y gets pruned away for having a free y. But, because of it's type, y is not really free.

Pruning non-Miller arguments¹ is however necessary to type-check even the current standard-library, so a blanket removal is not possible. So it should be done in such a way that variables of potentially singleton type² are not considered "bad".

¹. For example, applications of neutral constants, like type constructors or postulates.
². That is, variables that are definitionally equal to terms that do not contain them.

[andreasabel]

Related is #2625. The problem is that we have neutral terms of unit type which should be expanded to record{} to not be in the way of constraint solving. In MiniAgda, I eta-expanded such terms away, using a technique inspired by NbE (reflection, the up-arrow).
However, I am a bit unsure whether it is worthwhile being correct for the unit type, when these are more theoretical examples and the cost of getting rid of neutral terms of singleton type might be high.

However, the present issue might be easier to fix than #2625.

[vlopezj]

I wonder: now that Agda has instance arguments... is there a use case for having eta for the unit type? Apart from backwards compatibility. Andreas Abel <notifications@github.com> skrev: (20 december 2017 22:43:24 CET)

…

Related is #2625. The problem is that we have neutral terms of unit type which should be expanded to `record{}` to not be in the way of constraint solving. In MiniAgda, I etat-expanded such terms away, using a technique inspired by NbE (reflection, the up-arrow). However, I am a bit unsure whether it is worthwhile being correct for the unit type, when these are more theoretical examples and the cost of getting rid of neutral terms of singleton type might be high. -- You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub: #2876 (comment)

[nad]

I was thinking along the same lines.

[andreasabel]

For a start, you can try to "Keep your Neighbors in Order" with a unit data type instead of record see http://www.cse.chalmers.se/~abela/projects.html#agda

[nad]

I think it would be rather awkward to convert old code. Consider the following example:

record ⊤ : Set where
  no-eta-equality

instance
  tt : ⊤
  tt = record {}

record R : Set where
  field
    ⦃ f ⦄ : ⊤

works : R
works = record {}

fails : R
fails = _

Even if we change Agda so that the code above is accepted I would be reluctant to, say, mark the fields of Σ as instance arguments.

[andreasabel]

Yeah, that's the magic of the "singleton types" check which solves a meta if there is a unique inhabitant. (Not a complete check, but works for records.)