Replace SpecAtomType.pyClass with .ident, add BinaryIO, and align type mappings (#968)

Replace the `SpecAtomType.pyClass` variant with `.ident` using qualified
`PythonIdent`, add `typing.BinaryIO` support, and align PySpec→Laurel
type mappings with PythonToLaurel so non-primitive builtins map to `Any`
instead of lossy approximations.

## Changes

### 1. Fix missing source locations in PySpec translation errors
(`SourceRange.lean`, `Specs.lean`)

`SourceRange.format` crashed when called with a `none` range because it
unconditionally called `fm.toPosition` on zero offsets. Now it guards on
`isNone` and renders `"path:unknown"` instead. Several pattern matches
in `Specs.lean` were extracting annotated values via
`name.val`/`name.ann` but discarding the source location — these now
destructure as `⟨_, name⟩` at the binding site and pass the parent `loc`
to error reporters, ensuring translation errors always have usable
locations.

### 2. Remove `SpecAtomType.pyClass` variant (`Decls.lean`, `DDM.lean`,
`Specs.lean`, `ToLaurel.lean`)

`pyClass` stored an unqualified class name string, which was ambiguous
across modules. All construction sites now use `.ident` with a fully
qualified `PythonIdent` (module + name). DDM deserialization of legacy
`typeClass`/`typeClassNoArgs` Ion payloads produces `.ident` with empty
`pythonModule` for backward compatibility. All match arms and comparison
logic for `.pyClass` are removed.

### 3. Add `typing.BinaryIO` support (`Decls.lean`, `Specs.lean`,
`ToLaurel.lean`)

`BinaryIO` appears in boto3 stubs (e.g., `lambda_/client.py`'s `invoke`
returns `StreamingBody` typed as `BinaryIO`). Without this, pySpecs
throws "BinaryIO is not defined in module typing". Added
`PythonIdent.typingBinaryIO`, registered it in `preludeSig`, and mapped
it to `Any` in `knownIdentTypes`.

### 4. Align `knownIdentTypes` with PythonToLaurel (`ToLaurel.lean`)

Previously, PySpec→Laurel mapped types more aggressively than
PythonToLaurel: `bytes`/`bytearray`→`TString`, `complex`→`TReal`,
`dict`→`DictStrAny`, `Exception`→`Error`, `typing.List`→`ListStr`,
`typing.Dict`→`DictStrAny`. PythonToLaurel maps all of these to `Any`.
The mismatch meant pyspec-dispatched analysis could generate spurious
preconditions (e.g., string-length bounds on `bytes` parameters). Now
both paths agree: only `int`, `str`, `bool`, `float`, and `None` get
concrete Laurel types; everything else is `Any`.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: joehendrix

Strata/DDM/Util/SourceRange.lean

@@ -40,12 +40,15 @@ instance : Std.ToFormat SourceRange where
     Renders location information in a format VSCode understands.
     Returns "path:line:col-col" if on same line, otherwise "path:line:col". -/
 def format (loc : SourceRange) (path : System.FilePath) (fm : Lean.FileMap) : String :=
-  let spos := fm.toPosition loc.start
-  let epos := fm.toPosition loc.stop
-  if spos.line == epos.line then
-    s!"{path}:{spos.line}:{spos.column+1}-{epos.column+1}"
+  if loc.isNone then
+    s!"{path}:unknown"
   else
-    s!"{path}:{spos.line}:{spos.column+1}"
+    let spos := fm.toPosition loc.start
+    let epos := fm.toPosition loc.stop
+    if spos.line == epos.line then
+      s!"{path}:{spos.line}:{spos.column+1}-{epos.column+1}"
+    else
+      s!"{path}:{spos.line}:{spos.column+1}"
 
 end Strata.SourceRange
 end

Strata/Languages/Python/Specs.lean

@@ -205,11 +205,6 @@ private def SpecAtomType.toDDM (d : SpecAtomType)
       .typeIdentNoArgs loc nm.toDDM
     else
       .typeIdent loc nm.toDDM ⟨.none, args.map (·.toDDM)⟩
-  | .pyClass name args =>
-    if args.isEmpty then
-      .typeClassNoArgs loc ⟨.none, name⟩
-    else
-      .typeClass loc ⟨.none, name⟩ ⟨.none, args.map (·.toDDM)⟩
   | .intLiteral i => .typeIntLiteral loc (toDDMInt .none i)
   | .stringLiteral v => .typeStringLiteral loc ⟨.none, v⟩
   | .typedDict fields types fieldRequired =>
@@ -331,10 +326,10 @@ private def Signature.toDDM (sig : Signature) : DDM.Signature SourceRange :=
 private def DDM.SpecType.fromDDM (d : DDM.SpecType SourceRange) : Specs.SpecType :=
   match d with
   | .typeClassNoArgs loc ⟨_, cl⟩ =>
-    .ofAtom loc <| .pyClass cl #[]
+    .ident loc { pythonModule := "", name := cl } #[]
   | .typeClass loc ⟨_, cl⟩ ⟨_, args⟩ =>
     let a := args.map (·.fromDDM)
-    .ofAtom loc <| .pyClass cl a
+    .ident loc { pythonModule := "", name := cl } a
   | .typeIdentNoArgs loc ⟨_, ident⟩ =>
     if let some pyIdent := PythonIdent.ofString ident then
       .ident loc pyIdent #[]

Strata/Languages/Python/Specs/DDM.lean

@@ -25,6 +25,7 @@ def builtinsStr := mk "builtins" "str"
 def noneType := mk "_types" "NoneType"
 
 def typingAny := mk "typing" "Any"
+def typingBinaryIO := mk "typing" "BinaryIO"
 def typingDict := mk "typing" "Dict"
 def typingGenerator := mk "typing" "Generator"
 def typingList := mk "typing" "List"
@@ -77,7 +78,6 @@ An atomic type in the PySpec language
 -/
 inductive SpecAtomType where
 | ident (nm : PythonIdent) (args : Array SpecType)
-| pyClass (name : String) (args : Array SpecType)
 /- An integer literal -/
 | intLiteral (value : Int)
 /-- A string literal -/
@@ -127,7 +127,7 @@ termination_by a₁.size - i
 mutual
 
 /-- Compare two atom types by structure, ignoring `loc` in nested `SpecType`
-    values. Variants are ordered: ident < pyClass < intLiteral < stringLiteral
+    values. Variants are ordered: ident < intLiteral < stringLiteral
     < typedDict. -/
 protected def SpecAtomType.compare (x y : SpecAtomType) : Ordering :=
   match x, y with
@@ -137,12 +137,6 @@ protected def SpecAtomType.compare (x y : SpecAtomType) : Ordering :=
   | .ident .., _ => .lt
   | _, .ident .. => .gt
 
-  | .pyClass xname xargs, .pyClass yname yargs =>
-    compare xname yname |>.then $
-      compareHLex (fun ⟨xe, _⟩ ye => xe.compare ye) xargs.attach yargs
-  | .pyClass .., _ => .lt
-  | _, .pyClass .. => .gt
-
   | .intLiteral xval, .intLiteral yval => compare xval yval
   | .intLiteral .., _ => .lt
   | _, .intLiteral .. => .gt
@@ -262,9 +256,6 @@ protected def ofArray (loc : SourceRange) (atoms : Array SpecAtomType) : SpecTyp
 def ident (loc : SourceRange) (i : PythonIdent) (args : Array SpecType := #[]) : SpecType :=
   ofAtom loc (.ident i args)
 
-def pyClass (loc : SourceRange) (name : String) (params : Array SpecType) : SpecType :=
-  ofAtom loc (.pyClass name params)
-
 def asSingleton (tp : SpecType) : Option SpecAtomType := do
   if tp.atoms.size = 1 then
     for atp in tp.atoms do return atp

Strata/Languages/Python/Specs/Decls.lean

@@ -29,10 +29,6 @@ namespace WarningKind
 -- Type translation warnings
 def emptyType : WarningKind := { phase := "pySpecToLaurel", category := "emptyType" }
 def unsupportedUnion : WarningKind := { phase := "pySpecToLaurel", category := "unsupportedUnion" }
-def unknownType : WarningKind := { phase := "pySpecToLaurel", category := "unknownType" }
-def unsupportedGenericClass : WarningKind := { phase := "pySpecToLaurel", category := "unsupportedGenericClass" }
-def bytesToString : WarningKind := { phase := "pySpecToLaurel", category := "bytesToString" }
-def complexToReal : WarningKind := { phase := "pySpecToLaurel", category := "complexToReal" }
 
 -- Unsupported Optional patterns
 def unsupportedOptionalFloat : WarningKind := { phase := "pySpecToLaurel", category := "unsupportedOptionalFloat" }

Strata/Languages/Python/Specs/Error.lean

@@ -158,11 +158,6 @@ def atomTypeToString (a : SpecAtomType) : String :=
     else
       let argStrs := args.map specTypeToString
       s!"{nm}[{String.intercalate ", " argStrs.toList}]"
-  | .pyClass name args =>
-    if args.isEmpty then name
-    else
-      let argStrs := args.map specTypeToString
-      s!"{name}[{String.intercalate ", " argStrs.toList}]"
   | .intLiteral v => s!"Literal[{v}]"
   | .stringLiteral v => s!"Literal[\"{v}\"]"
   | .typedDict _ _ _ => "TypedDict"
@@ -255,25 +250,24 @@ def detectOptionalType (ty : SpecType) : ToLaurelM (Option HighTypeMd) := do
     return none
 
 /-- Known PythonIdent → Laurel type mappings for single-atom ident types.
-    - `bytes`/`bytearray` → TString (closest string-like approximation)
-    - `complex` → TReal (no complex type in SMT; real is the closest numeric type)
-    - `Exception` → UserDefined "Error" (matches CorePrelude's Error datatype)
-    - `typing.Any` → UserDefined "Any" (datatype in Laurel prelude) -/
+    Matches PythonToLaurel's type mapping: only int, str, bool, float get
+    concrete Laurel types; everything else maps to Any. -/
 private def knownIdentTypes : Std.HashMap PythonIdent HighTypeMd :=
   .ofList [
     (.builtinsBool,      tyBool),
-    (.builtinsBytearray, tyString),
-    (.builtinsBytes,     tyString),
-    (.builtinsComplex,   tyReal),
-    (.builtinsDict,      tyDictStrAny),
-    (.builtinsException, tyError),
+    (.builtinsBytearray, tyAny),
+    (.builtinsBytes,     tyAny),
+    (.builtinsComplex,   tyAny),
+    (.builtinsDict,      tyAny),
+    (.builtinsException, tyAny),
     (.builtinsFloat,     tyReal),
     (.builtinsInt,       tyInt),
     (.builtinsStr,       tyString),
     (.noneType,          tyVoid),
     (.typingAny,         tyAny),
-    (.typingDict,        tyDictStrAny),
-    (.typingList,        tyListStr),
+    (.typingBinaryIO,    tyAny),
+    (.typingDict,        tyAny),
+    (.typingList,        tyAny),
   ]
 
 /-- Convert a SpecType to a Laurel HighTypeMd. -/
@@ -306,20 +300,9 @@ def specTypeToLaurelType (ty : SpecType) : ToLaurelM HighTypeMd := do
     -- Single atom type
     match ty.atoms[0]! with
     | .ident nm _args =>
-      -- Warn for lossy known-type approximations
-      if nm == .builtinsBytes || nm == .builtinsBytearray then
-        reportError .bytesToString default s!"'{nm}' mapped to TString (bytes have different semantics)"
-      if nm == .builtinsComplex then
-        reportError .complexToReal default s!"'{nm}' mapped to TReal (complex loses imaginary component)"
       if let some ty := knownIdentTypes[nm]? then
         return ty
-      reportError .unknownType default s!"Unknown type '{nm}' mapped to TString"
-      return tyString
-    | .pyClass name args =>
-      if args.size > 0 then
-        reportError .unsupportedGenericClass default
-          s!"Generic class '{name}' with type args unsupported"
-      let prefixed ← prefixName name
+      let prefixed ← prefixName nm.name
       return mkTy (.UserDefined { text := prefixed, md := .empty })
     | .intLiteral _ => return tyInt
     | .stringLiteral _ => return tyString
@@ -671,9 +654,8 @@ def typeDefToLaurel (td : TypeDef) : ToLaurelM Unit := do
   })
 
 /-- Extract an overload dispatch entry from an `@overload` function declaration.
-    Looks for a `stringLiteral` in the first argument's type and a class
-    return type (either `.pyClass` for locally-defined classes or `.ident`
-    for externally imported classes), and records them in the dispatch table. -/
+    Looks for a `stringLiteral` in the first argument's type and an `.ident`
+    return type, and records them in the dispatch table. -/
 def extractOverloadEntry (func : FunctionDecl) : ToLaurelM Unit := do
   let args := func.args.args
   let .isTrue _ := decideProp (args.size > 0)
@@ -703,10 +685,6 @@ def extractOverloadEntry (func : FunctionDecl) : ToLaurelM Unit := do
       return
   let retType ←
         match func.returnType.atoms[0] with
-        | .pyClass name _ => do
-          let ctx ← read
-          let prefixed ← prefixName name
-          pure (PythonIdent.mk ctx.modulePrefix prefixed)
         | .ident nm _ => pure nm
         | _ =>
           reportError .overloadReturnNotClass func.loc

Strata/Languages/Python/Specs/ToLaurel.lean

@@ -12,9 +12,8 @@ namespace DeclsTest
 private abbrev mk1 (a : SpecAtomType) : SpecType := ⟨#[a], ⟨0, 0⟩⟩
 private abbrev mk2 (a : SpecAtomType) : SpecType := ⟨#[a], ⟨⟨1⟩, ⟨2⟩⟩⟩
 
--- Atom ordering: ident < pyClass < intLiteral < stringLiteral < typedDict
-#guard compare (SpecAtomType.ident .builtinsInt #[]) (.pyClass "Foo" #[]) == .lt
-#guard compare (SpecAtomType.pyClass "Foo" #[]) (.intLiteral 0) == .lt
+-- Atom ordering: ident < intLiteral < stringLiteral < typedDict
+#guard compare (SpecAtomType.ident .builtinsInt #[]) (.intLiteral 0) == .lt
 #guard compare (SpecAtomType.intLiteral 0) (.stringLiteral "a") == .lt
 
 -- Same variant compares by fields

StrataTest/Languages/Python/Specs/DeclsTest.lean

@@ -79,7 +79,7 @@ class "MainClass" {
   exhaustive: false
   function "main_method"{
     args: [
-      self : class(MainClass) [default: ]
+      self : ident("main.MainClass") [default: ]
       x : ident("basetypes.BaseClass") [default: ]
     ]
     kwonly: [
@@ -94,7 +94,7 @@ class "MainClass" {
 }
 function "main_function"{
   args: [
-    x : class(MainClass) [default: ]
+    x : ident("main.MainClass") [default: ]
   ]
   kwonly: [
   ]
@@ -186,7 +186,7 @@ class "InnerHelper" {
 class "ClassWithInit" {
   bases: []
   fields: [
-    helper : class(_InnerHelper) "_InnerHelper()"
+    helper : ident("main._InnerHelper") "_InnerHelper()"
   ]
   classVars: []
   subclasses: [
@@ -198,7 +198,7 @@ class "ClassWithInit" {
       exhaustive: false
       function "do_work"{
         args: [
-          self : class(_InnerHelper) [default: ]
+          self : ident("main._InnerHelper") [default: ]
         ]
         kwonly: [
         ]

StrataTest/Languages/Python/SpecsTest.lean

@@ -156,10 +156,10 @@ procedure with_kwonly(x:TInt, verbose:TBool) returns(result:TString)
 
 /--
 info: procedure takes_any(x:UserDefined(Any)) returns(result:TInt)
-procedure takes_list(items:UserDefined(ListStr)) returns(result:TBool)
-procedure returns_dict() returns(result:UserDefined(DictStrAny))
-procedure typed_list() returns(result:UserDefined(ListStr))
-procedure typed_dict() returns(result:UserDefined(DictStrAny))
+procedure takes_list(items:UserDefined(Any)) returns(result:TBool)
+procedure returns_dict() returns(result:UserDefined(Any))
+procedure typed_list() returns(result:UserDefined(Any))
+procedure typed_dict() returns(result:UserDefined(Any))
 -/
 #guard_msgs in
 #eval runTest #[
@@ -229,10 +229,10 @@ procedure opt_int_enum() returns(result:UserDefined(IntOrNone))
 /-! ## Error cases (updated to verify WarningKind) -/
 
 /--
-info: pySpecToLaurel.unknownType: Unknown type 'foo.Bar' mapped to TString
+info: procedure f() returns(result:UserDefined(Bar))
 -/
 #guard_msgs in
-#eval runTestWarningKinds
+#eval runTest
   #[mkFuncSig "f"
     (identType (PythonIdent.mk "foo" "Bar"))]
 
@@ -317,8 +317,8 @@ procedure uses_class(x:UserDefined(Foo)) returns(result:UserDefined(Foo))
     loc := loc, name := "Foo"
     methods := #[]
   },
-  mkFuncSig "uses_class" (.pyClass loc "Foo" #[])
-    (args := #[mkArg "x" (.pyClass loc "Foo" #[])])
+  mkFuncSig "uses_class" (mkType (.ident (PythonIdent.mk "" "Foo") #[]))
+    (args := #[mkArg "x" (mkType (.ident (PythonIdent.mk "" "Foo") #[]))])
 ]
 
 /-! ## Empty input -/
@@ -407,7 +407,7 @@ dispatch create_client:
   mkFuncSig "helper" (identType .builtinsBool)
 ]
 
--- Overloads with locally-defined class return types (.pyClass).
+-- Overloads with locally-defined class return types.
 /--
 info: type Alpha
 type Beta
@@ -419,9 +419,9 @@ dispatch make:
 #eval runFullTest #[
   .classDef { loc := loc, name := "Alpha", methods := #[] },
   .classDef { loc := loc, name := "Beta", methods := #[] },
-  mkOverload "make" (.pyClass loc "Alpha" #[])
+  mkOverload "make" (mkType (.ident (PythonIdent.mk "" "Alpha") #[]))
     (args := #[mkArg "kind" (mkType (.stringLiteral "a"))]),
-  mkOverload "make" (.pyClass loc "Beta" #[])
+  mkOverload "make" (mkType (.ident (PythonIdent.mk "" "Beta") #[]))
     (args := #[mkArg "kind" (mkType (.stringLiteral "b"))])
 ]
 
@@ -502,36 +502,26 @@ body contains FieldSelect: false
 
 /-! ## Warning kind tests -/
 
--- Type translation: unsupportedGenericClass
+-- bytes, bytearray, complex now map to Any (matching PythonToLaurel)
 /--
-info: pySpecToLaurel.unsupportedGenericClass: Generic class 'Foo' with type args unsupported
+info: procedure f() returns(result:UserDefined(Any))
 -/
 #guard_msgs in
-#eval runTestWarningKinds
-  #[mkFuncSig "f" (mkType (.pyClass "Foo" #[identType .builtinsInt]))]
-
--- Type translation: bytesToString
-/--
-info: pySpecToLaurel.bytesToString: 'builtins.bytes' mapped to TString (bytes have different semantics)
--/
-#guard_msgs in
-#eval runTestWarningKinds
+#eval runTest
   #[mkFuncSig "f" (identType .builtinsBytes)]
 
--- Type translation: bytesToString (bytearray variant)
 /--
-info: pySpecToLaurel.bytesToString: 'builtins.bytearray' mapped to TString (bytes have different semantics)
+info: procedure f() returns(result:UserDefined(Any))
 -/
 #guard_msgs in
-#eval runTestWarningKinds
+#eval runTest
   #[mkFuncSig "f" (identType .builtinsBytearray)]
 
--- Type translation: complexToReal
 /--
-info: pySpecToLaurel.complexToReal: 'builtins.complex' mapped to TReal (complex loses imaginary component)
+info: procedure f() returns(result:UserDefined(Any))
 -/
 #guard_msgs in
-#eval runTestWarningKinds
+#eval runTest
   #[mkFuncSig "f" (identType .builtinsComplex)]
 
 -- Unsupported Optional patterns