Defaulting not working for pattern let-bindings at REPL

[brianhuffman]

Cryptol> let (x, y) = (3, 4)

[error] at <interactive>:1:1--1:7:
  Unsolved constraints:
    Literal 3 ?<interactive>::x`862
      arising from
      use of expression <interactive>::__p0
      at <interactive>:1:1--1:7
  where
  ?<interactive>::x`862 is the type of '<interactive>::x' at <interactive>:1:5--1:20
[error] at <interactive>:1:1--1:10:
  Unsolved constraints:
    Literal 4 ?<interactive>::y`868
      arising from
      use of expression <interactive>::__p0
      at <interactive>:1:1--1:10
  where
  ?<interactive>::y`868 is the type of '<interactive>::y' at <interactive>:1:5--1:20

On the other hand, if you put (x, y) = (3, 4) in a file, defaulting works properly:

Loading module Cryptol
Loading module Main
[warning] at :1:1--1:16:
  Defaulting the type of 'Main::y' to [3]
[warning] at :1:1--1:16:
  Defaulting the type of 'Main::x' to [2]

This whole problem leaves me wondering, why do x and y need to have monomorphic types here? It seems like this might be related to #534 somehow.

[elliottt]

This might be related to the decision to make declarations in the where clause monomorphic. Do you still get the problem if you do :set mono-binds=false before?

[brianhuffman]

Setting mono-binds=false doesn't change the error.

[yav]

The x and y being monomorphic is by design, although looking at the NoPat translation, things can be improved.

The thinking was that when you have a pattern binding, usually you want the bound variables to refer to the same instantiation of the RHS. For example, if I write x # y = e I would like the x and y to have types that are related to each other (i.e., they have to be instantiated together). Since we don't have a construct that allows multiple things to be instantiated at once, we just keep them monomorphic.

I'll have a look at the defaulting and the command-line let, I am not sure how that works, but it is likely that this is an artifact of how let is implement.