Unification issue for indices

Stream: lean4

[Jakob von Raumer]

So this is not working but we really would like it to (it appears in an automatically generated file, that's why there's an unreduced index in the binder):

example : BitVec (4 * 4) :=
  BitVec.append (BitVec.zero 2) (BitVec.zero 14)

example (α : Type) (a : α) : Vector α (4 * 4) :=
  Vector.append (Vector.mkVector 2 a) (Vector.mkVector 14 a)

This really should work, shouldn't it? :thinking:

[Jakob von Raumer]

(What happens is probably that 4 * 4 is unfolded to 4 * 3 + 4 once and that decomposition is unified with the index of the return type of append)

[Jakob von Raumer]

Having an explicit coercion works, but is that the best workaround?

[Joachim Breitner]

Strange indeed. And (JFTR, not surprising) not specific to BitVec:

-- set_option trace.Meta.isDefEq true

axiom BV : Nat → Type
axiom BV.zero n : BV n
axiom BV.append {n m} : BV n → BV m → BV (n + m)

/--
error: application type mismatch
  (BV.zero 2).append
argument
  BV.zero 2
has type
  BV 2 : Type
but is expected to have type
  BV (Nat.mul 4 3) : Type
-/
#guard_msgs in
noncomputable example : BV (4 * 4) :=
  BV.append (BV.zero 2) (BV.zero 14)

#guard_msgs in
noncomputable example : BV (4 * 4) :=
  BV.append (BV.zero 12) (BV.zero 4)

[Joachim Breitner]

You don't need a coercion, even a type ascription helps:

noncomputable example : BV (4 * 4) :=
  (BV.append (BV.zero 2) (BV.zero 14) : BV 16)

[Joachim Breitner]

It is also not Nat-specific (which I would not have been surprised about):

-- set_option trace.Meta.isDefEq true

inductive MyNat where | zero | succ : MyNat → MyNat
def MyNat.add : MyNat → MyNat → MyNat
  | a, .zero   => a
  | a, .succ b => .succ (.add a b)
def MyNat.mul : MyNat → MyNat → MyNat
  | _, .zero   => .zero
  | a, .succ b => .add (.mul a b) a

def two := MyNat.zero.succ.succ.succ.succ
def four := MyNat.zero.succ.succ.succ.succ
def fourteen := MyNat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ

axiom BV : MyNat → Type
axiom BV.zero n : BV n
axiom BV.append {n m} : BV n → BV m → BV (.add n m)

/--
error: application type mismatch
  (BV.zero two).append
argument
  BV.zero two
has type
  BV two : Type
but is expected to have type
  BV (four.mul MyNat.zero.succ.succ.succ) : Type
-/
#guard_msgs in
noncomputable example : BV (.mul four four) :=
  BV.append (BV.zero two) (BV.zero fourteen)

[Jakob von Raumer]

Yes, I think it's a generic effect of the unification order

[Eric Wieser]

No coercion required:

example : BitVec (4 * 4) :=
  (BitVec.append (BitVec.zero 2) (BitVec.zero 14) :)

[Jakob von Raumer]

What's :), just a vacuous type annotation?

[Joachim Breitner]

Jakob von Raumer said:

Yes, I think it's a generic effect of the unification order

It seems to be assigning metavariables during “lazy“ unification:

Meta.isDefEq] ✅️ BV (four.mul four) =?= BV (MyNat.add ?m.778 ?m.779) ▼
  [] ✅️ four.mul four =?= MyNat.add ?m.778 ?m.779 ▼
    [] ✅️ (four.mul MyNat.zero.succ.succ.succ).add four =?= MyNat.add ?m.778 ?m.779 ▼
      [] ✅️ four.mul MyNat.zero.succ.succ.succ =?= ?m.778 ▼
        [] four.mul MyNat.zero.succ.succ.succ [nonassignable] =?= ?m.778 [assignable]
        [] ✅️ MyNat =?= MyNat
      [] ✅️ four =?= ?m.779 ▼
        [] four [nonassignable] =?= ?m.779 [assignable]
        [] ✅️ MyNat =?= MyNat

[Kyle Miller]

@Jakob von Raumer (e :) elaborates e completely (synthesizing instances and all that), and only then does it take the expected type into account, unifying the type of e with the expected type and otherwise inserting a coercion. On the other hand, (e : t) elaborates e using t as the expected type, inserting a coercion if the types don't line up.

[Tomas Skrivan]

By changing the signature of Vector.append you can also get the reduction (2+14 ==> 16) in the type automatically

import Lean

open Lean Std

def Vector.append' (x : Vector α n) (y : Vector α m) {mn} (hmn : mn = n + m := by (conv => rhs; simp); try rfl) : Vector α mn :=
  hmn ▸ x.append y

example (α : Type) (a : α) : Vector α (4 * 4) :=
  Vector.append' (Vector.mkVector 2 a) (Vector.mkVector 14 a)

Also

#check Vector.append' (Vector.mkVector 2 a) (Vector.mkVector 14 a)

is of type Vector α 16 and not Vector α (2+14)

[Jakob von Raumer]

@Tomas Skrivan I've employed this trick before, but it always feels a bit dirty, especially if you'd have to wrap multiple of such functions.
dsimp only is probably enough, right?

[Kim Morrison]

This couldn't replace the definition of Vector.append, but it is tempting to add it as a variant.

[Jakob von Raumer]

I understand, but it's unclear for how many operation we'd have to add such a wrapper. BitVec.replicate seems prone to the same effect, with pow and mul instead of mul and add, for example...

[Jakob von Raumer]

Jakob von Raumer said:

I understand, but it's unclear for how many operation we'd have to add such a wrapper. BitVec.replicate seems prone to the same effect, with pow and mul instead of mul and add, for example...

Hmm, I can't actually expose the same thing with BitVec.replicate, that's weird

[Leo Stefanesco]

We have found another strange unification failure:

def Sail.BitVec.updateSubrange
  {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + 1))
  : BitVec w := by sorry

def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) :=
  (Sail.BitVec.updateSubrange v (8 - 1) 0 x)

fails with

application type mismatch
  Sail.BitVec.updateSubrange v (8 - 1) 0 x
argument
  x
has type
  BitVec 8 : Type
but is expected to have type
  BitVec (8 - 1 - 0 + 1) : Type

Apparently this used to works with lean 4.14

[James Gallicchio]

further minimized:

opaque MyTy (n : Nat) : Type
opaque foo (hi) (_y : MyTy (hi + 1)) : Unit

set_option trace.Meta.isDefEq true

def bar (x : MyTy 8) := foo (8-1)
                          x   -- type error
def bar' (x : MyTy 8) := foo (HSub.hSub 8 1)
                          x   -- succeeds

It is surprising to me that Nat.sub behaves different from the notation. The isDefEq traces encounter the same goal in both, but bar' continues where bar' fails, so I assume this is some defeq heuristic messing up?

[Yakov Pechersky]

Is there an elaboration issue of inferring the type of 8-1 that you sidestep by the explicit Nat in bar'?

[Jakob von Raumer]

Yakov Pechersky said:

Is there an elaboration issue of inferring the type of 8-1 that you sidestep by the explicit Nat in bar'?

I don't think that's the issue, the trace looks like it seems to figure out that it's Nat before the failure. For some reason when looking at (Nat.sub 8 0).pred it matches on Nat.sub 8 0 without ever reducing it, that seems to be part of the issue