Size-synonyms do not unify

[bgamari]

In my program I have found it helpful to write local synonyms of my sizes to keep type signatures of let bindings manageable. For instance,

module S = { def n : i64 = 42 }

def hi: [42]f32 =
  let n = S.n
  let y0 : [n]f32 = rep 0
  let y1 : [S.n]f32 = y0
  in y1

However, this is rejected with:

Loading tmp.fut
Error at tmp.fut:8:7-20:
Pattern
  y1: [S.n]f32
cannot match value of type
  [n]f32

Sizes "S.n" and "n" do not match.

Is this expected?

[athas]

The type checker does not perform any substitutions (or otherwise interpret expressions in any way, except for ignoring parentheses), so this is expected and unfortunate. I think this could eventually be fixed without running into the issues discussed in https://futhark-lang.org/blog/2023-05-12-size-type-challenges.html#unification