Unification of decoding functions

[atennapel]

In "Dependently Typed Programming in Agda" (P33) a universe for overloading is shown. Let me give a minimal example (in Agda-like syntax):

TYPE : * = Bool
BOOL : TYPE = True
NAT : TYPE = False

decode : TYPE -> * = \t. if t then Bool else Nat

eq : (t : TYPE) -> decode t -> decode t -> Bool
= \t. indBool (\t. decode t -> decode t -> Bool) eqBool eqNat t

eq BOOL True False == False
eq NAT 1 1 = True

Now in Agda apparently the TYPE can be inferred. But in the system of this repo obviously it will not:

eq _ 1 1
Results in the unification:
Nat ~ decode ?1
Which then tries to solve (with if-then being the eliminator in the spine):
?1 (if-then Bool else Nat) := Nat

This fails because there is an eliminator in the spine of ?1. Now I can see a way to solve this in this special case because if-then has exactly two possible results, so we could try to unify the results and see:

try Bool
Bool := Nat
fail
try Nat
Nat := Nat
success
solve ?1 := False

Does this seem like a reasonable thing to add to you, in order to beef up the unification in some cases? Or do you know of a more general approach to try and solve problems like this?

[AndrasKovacs]

This is already supported in current Agda. See e.g. section 5 of this ("invertible problems"). I think it definitely works in Agda 2.6.1 if decode is defined with pattern matching, otherwise I'm not sure. It does not lose any unification solutions if implemented conservatively, so it's a reasonable thing to add.

[atennapel]

Thanks for the reference!

[ollef]

FWIW, Sixty has this kind of conservative case inversion ~hacked in~ implemented.

It's sometimes surprisingly powerful.

[atennapel]

Yeah that's awesome! So in your case I see in:

case scrutinee of
  con1 vs1 -> con1' es1
  con2 vs2 -> con2' es2
==
con1' es1'

The con1' is matched by a simple equality check of the constructor? So no unification/backtracking there.

[ollef]

Yeah, that's right. It's a quite superficial test to avoid backtracking.

[atennapel]

This is where having native datatypes and a pattern matching construct also seems to make things easier. In "Gentle art of levitation" and my system (unit, bool, fix) even a simple sum type A + B is (b : Bool) ** if b then A else B, which makes the same equation look more like ?0 fst (if-then (\a. v1) (\b. v2)) (snd ?0) == v.