[spectec] Ambiguous expression juxtaposition

[zilinc]

In the following sample code,

var n : nat  ;; <--- problematic

def $f(nat*) : nat
def $f(n*) = n'
  -- if n* = n_1'* n_2*
  -- if n_1'* = n_1* n'

With the var declaration, it's elaborated into:

;; juxt.spectec:3.1-3.19
def $f(nat*) : nat
  ;; juxt.spectec:4.1-6.24
  def $f{`n*` : nat*, n' : nat, `n_1'*` : nat*, `n_2*` : nat*, `n_1*` : nat*}(n*{n <- `n*`}) = n'
    -- if ([n*{n <- `n*`}] = [n_1'*{n_1' <- `n_1'*`} n_2*{n_2 <- `n_2*`}])
    -- if (n_1'*{n_1' <- `n_1'*`} = n_1*{n_1 <- `n_1*`} ++ [n'])

Whereas if we comment out the var declaration, it's elaborated into:

;; juxt.spectec:3.1-3.19
def $f(nat*) : nat
  ;; juxt.spectec:4.1-6.24
  def $f{`n*` : nat*, n' : nat, `n_1'*` : nat*, `n_2*` : nat*, `n_1*` : nat*}(n*{n <- `n*`}) = n'
    -- if (n*{n <- `n*`} = n_1'*{n_1' <- `n_1'*`} ++ n_2*{n_2 <- `n_2*`})
    -- if (n_1'*{n_1' <- `n_1'*`} = n_1*{n_1 <- `n_1*`} ++ [n'])

The variable declaration doesn't change the result of the type inference, but the ILs have totally different semantics.

[rossberg]

Yeah, I know where the problem is. When the elaborator sees a sequence in inference mode, and succeeds for the individual expressions (because n was declared), then it just takes that as a list of elements. That is not principal, and there is a comment to that regard in the code. (When inference fails, however, it backtracks and infers the l.h.s. of the equation first, such that it can run the r.h.s. in checking mode, which does the right thing.)

I fixed this by only allowing that inference in the unambiguous case where the element type is not itself a list type. PTAL at #2160.