invalid pattern, constructor or constant marked with '[match

Stream: lean4

[Chris Lovett]

What does this error mean, I copied this code straight from Lean json parser, but it doesn't compile in my own little sample:

import Lean.Data.Json
open Lean (Json)

def formatMarkdown (j: Json) : String :=
  match j with
  | null       => "null"
  | bool true  => "true"
  | bool false => "false"
  | num s      => s.toString
  | _          => "error"

saying invalid pattern, constructor or constant marked with '[matchPattern]' expected on the bool true, if I remove those it says the same thing on num s? What am I doing wrong?

[James Gallicchio]

Seems like a namespace issue? If you add . in front of the patterns (.bool true) does it work?

[James Gallicchio]

I'm not sure what the open Lean (Json) syntax actually does, but if the constructors aren't in top-level scope then you need to qualify them with a ., either specifying the namespace they come from (Json.null etc) or letting Lean fill in the namespace based on j's type (.null etc)

[James Gallicchio]

I'm guessing here that Lean is interpreting the first line as a variable pattern, not a constructor, which is why it doesn't complain about the first case?

[Mario Carneiro]

The open Lean (Json) syntax means to make only Lean.Json available by the short name Json, not any of the Lean.Json.foo constructors

[Mario Carneiro]

open Lean Json is closer to what you want

[Chris Lovett]

Oh, you are right, if I fully qualify the cases then it works fine. Super confusing error message... so this works:

  match j with
  | Json.null => IO.println "Error: unexpected null type"
  | Json.bool b => IO.println "Error: unexpected boolean type"
  | Json.num n => IO.println "Error: unexpected number type"
  | Json.str s => IO.println "Error: unexpected string type"
  | Json.arr a => IO.println "Error: unexpected array type"
  | Json.obj o => IO.println "Yay"

[Chris Lovett]

Even if I just add dots it works fine:

  match j with
  | .null => IO.println "Error: unexpected null type"
  | .bool b => IO.println "Error: unexpected boolean type"
  | .num n => IO.println "Error: unexpected number type"
  | .str s => IO.println "Error: unexpected string type"
  | .arr a => IO.println "Error: unexpected array type"
  | .obj o => IO.println "Yay"

[Mario Carneiro]

but if you are not in namespace Lean.Json, you still won't be able to write bool because there is an ambiguity with the _root_.bool definition

[Mario Carneiro]

Certainly using prefix dots is the easiest way to avoid messing about with namespaces / open

[James Gallicchio]

And it's also just good style to always have the ., to avoid Lean re-interpreting a constructor pattern as a variable pattern. Seems very worth it for one extra character