AssocList "failed to synthesize"

Stream: lean4

[Zygimantas Straznickas]

import Std.Data.AssocList

def l : List (Prod Nat Nat) := [(1, 1), (2, 2)]
#eval l -- works
#eval (List.toAssocList l) -- failed to synthesize Lean.Eval (Std.AssocList Nat Nat)

possible bug?

[Mario Carneiro]

I would guess that Lean.Eval means something like lean 3's has_repr, a way to print the resulting data structure

[Mario Carneiro]

In other words, while lean can compute the AssocList, it doesn't know how to show the result

[Bryan Gin-ge Chen]

This was a fun little exercise:

import Std.Data.AssocList

def l : List (Prod Nat Nat) := [(1, 1), (2, 2)]
#eval l -- works

def Std.AssocList.ToList : AssocList α β → List (α × β)
  | AssocList.nil => []
  | AssocList.cons k v t => (k, v) :: ToList t

instance [Repr α] [Repr β] : Repr (Std.AssocList α β) where
  reprPrec f _ := repr f.ToList

#eval (l.toAssocList) -- works

[Zygimantas Straznickas]

Thanks! I'm coming from Coq so my knowledge of Lean 3 is limited :) Is there a way to just see the fully reduced term? I tried #reduce (in Lean 4) but in this example it gives me

Std.AssocList.cons 1 1
  { fst :=
          List.rec
            { fst :=
                (fun (t : List (Nat × Nat)) (f : List.below t) =>
                    (match t with
                      | [] => fun (x : List.below []) => Std.AssocList.nil
                      | (a, b) :: es => fun (x : List.below ((a, b) :: es)) => Std.AssocList.cons a b x.fst.fst)
                      f)
                  [] PUnit.unit,
              snd := PUnit.unit }
            (fun (head : Nat × Nat) (tail : List (Nat × Nat))
              (v_0 : PProd ((fun (x : List (Nat × Nat)) => Std.AssocList Nat Nat) tail) (List.below tail)) =>
              { fst :=
                  (fun (t : List (Nat × Nat)) (f : List.below t) =>
                      (match t with
                        | [] => fun (x : List.below []) => Std.AssocList.nil
                        | (a, b) :: es => fun (x : List.below ((a, b) :: es)) => Std.AssocList.cons a b x.fst.fst)
                        f)
                    (head :: tail) { fst := v_0, snd := PUnit.unit },
                snd := { fst := v_0, snd := PUnit.unit } })
            [(2, 2)],
        snd := PUnit.unit }.fst.fst

instead of the expected cons 1 1 (cons 2 2 nil)

[Zygimantas Straznickas]

hmm, #reduce fully reduces this in Lean 3

[Mario Carneiro]

It appears that lean 4 #reduce isn't actually full reduction, it is just doing whnf

[Mario Carneiro]

if you peel off the top level constructor it will continue to make progress