Problem typing a let expression

[desfreng]

Description

Hi ! I've been playing around with PureScript's typing system and I've come across an example where the compiler's behaviour doesn't seem consistent.

In my experiments and as mentioned in ticket #4498, PureScript does not generalise let expressions. So why is the following code accepted by the compiler? The reasons why I think this code should not be accepted are in the comments to the following code.

module Main where

import Prelude (class Show, Unit, discard, show, (<>))
import Effect (Effect)
import Effect.Console (log)

data List a = Nil | Cons a (List a)

instance (Show a) => Show (List a) where
  show (Nil) = "Nil"
  show (Cons hd tl) = "(Cons " <> show hd <> " " <> show tl <> ")"

main :: Effect Unit
main = let x = Nil in -- x :: List τ, with τ unknown at this point
  do
    (let y = Cons "a" x in log (show y)) -- Here we find that τ = String, so x :: List String
    (let z = Cons true x in log (show z)) -- Boolean /= String, so why no error is repported here ?

The error is correctly emitted when the arity of the List type is modified :

module Main where

import Prelude (class Show, Unit, discard, show, (<>))
import Effect (Effect)
import Effect.Console (log)

data List a b = Nil a | Cons b (List a b)

instance (Show a, Show b) => Show (List a b) where
  show (Nil x) = "(Nil " <> show x <> ")"
  show (Cons hd tl) = "(Cons " <> show hd <> " " <> show tl <> ")"

main :: Effect Unit
main = let x = Nil 1 in -- x :: List Int τ, with τ unknown at this point
  do
    (let y = Cons "a" x in log (show y)) -- Here we find that τ = String, so x :: List Int String
    (let z = Cons true x in log (show z)) -- Boolean /= String, so we GET an error repported here.

To Reproduce

To reproduce this problem, simply copy-paste each of the examples into the Main.purs file generated by spago init, then call spago build.
You can also use try.purescript.org :

• Code snippet 1 (without the expected error)
• Code snippet 2 (with the correct error)

Expected behavior

I expected the compiler to behave consistently, regardless of the arity of the List type introduced. That is, an error would be returned at the point explained in the comments in the first code snippet.

PureScript version

v0.15.13 (with try.purescript.org) and v0.15.12 (on my computer).

[natefaubion]

Probably #3874 I don't know if it's generalization so much as Nil is an identifier with a known type so it just accepts it's type as-is (lazy instantiation).