Why does not declaring `main` type cause this error?

Stream: new members

[Dan Abramov]

This typechecks:

def main := do
  IO.print "Enter your name: "
  let stdin ← IO.getStdin
  let name ← stdin.getLine
  IO.println ("Hello, " ++ name)

Now let's remove the first print. Suddenly it doesn't:

def main := do
  let stdin ← IO.getStdin
  let name ← stdin.getLine
/--
type mismatch
  stdin.getLine
has type
  IO String : Type
but is expected to have type
  BaseIO ?m.10048 : Type
--/
  IO.println ("Hello, " ++ name)

I can fix it by adding : IO Unit though:

def main : IO Unit := do
  let stdin ← IO.getStdin
  let name ← stdin.getLine
  IO.println ("Hello, " ++ name)

How do I make sense of this? What is the chain of inferences that breaks this?

I'm asking both because it would kind of feel neater to not have to write : IO Unit, and because I don't understand what's happening. I was actually stuck on this error message for a while.

[Aaron Liu]

probably some sort of monad lift stuff

[Aaron Liu]

IO.getStdin is guaranteed to never error, and that is reflected in its return type being BaseIO instead of IO

[Aaron Liu]

but that also means when you bind it you need to convert the BaseIO into IO

[Aaron Liu]

and that is usually done automatically

[Aaron Liu]

but this time it wasn't done because we didn't know it had to be converted since there was no expected type

[Eric Wieser]

The other consideration here is that main is not special when it comes to type-checking, and so there is no expected type available of the form "well this is the main function so it must be IO"

[Dan Abramov]

Thanks. Is there any other place I could've done this annotation? Purely scientific interest. I tried putting IO in a few places but I'm not sure I understand which type is flowing where.

[Dan Abramov]

I've tried

def main := do
  let stdin ← (IO.getStdin: IO IO.FS.Stream)
  let name ← stdin.getLine
  IO.println ("Hello, " ++ name)

but now the problem is it's being inferred as EIO IO.Error Unit which I'm not sure where it's coming from.

[Eric Wieser]

This works:

def main := do
  let stdin ← liftM <| IO.getStdin
  let name ← stdin.getLine
  IO.println ("Hello, " ++ name)

[Eric Wieser]

Dan Abramov said:

but now the problem is it's being inferred as EIO IO.Error Unit which I'm not sure where it's coming from.

IO Unit = EIO IO.Error Unit is true by definition

[Eric Wieser]

I think this error message is a bug

[Eric Wieser]

Something somewhere is saying "is the type exactly IO Unit?", but should probably be saying "Is the type reducibly defeq to IO Unit?".