peculiar universal quantification on inferred type of delayed function

[atacratic]

Slurp the following:

ability SystemTime where
  systemTime : .base.Nat

tomorrow = '(SystemTime.systemTime + 24 * 60 * 60)

You get:

  ✅
  
  I found and typechecked these definitions in ~/u1/scratch.u. If you do an
  `add` or `update` , here's how your codebase would change:
  
    ⍟ These new definitions are ok to `add`:
    
      ability SystemTime
      tomorrow : ∀ (). () ->{SystemTime} .base.Nat
  
  Now evaluating any watch expressions (lines starting with `>`)...
  Ctrl+C cancels.

Note the ∀ () in the inferred signature for tomorrow. Surely there's only one () unit type, we don't need to quantify? I'd expect it to infer tomorrow : () ->{SystemTime} .base.Nat

(M1a)

[atacratic]

Correction: I'd expect the inferred type to be printed as tomorrow : '{SystemTime} .base.Nat, i.e. with the delay sugar.

[aryairani]

It doesn't matter that there's only one () unit type, since it's being shadowed by the one introduced in the forall. (This is related to the discussion at #642.)

Correction: I'd expect the inferred type to be printed as tomorrow : '{SystemTime} .base.Nat, i.e. with the delay sugar.

Agreed!

[atacratic]

Plus the version that comes out with the () in the quantification doesn't successfully parse: #1538