From c8a67165a706bbfa23f1c3e85d1b0154f28c554b Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 15 Jun 2026 17:04:41 +0100 Subject: [PATCH] =?UTF-8?q?fix(abi/idris):=20make=20Types.idr=20typecheck?= =?UTF-8?q?=20total=20=E2=80=94=20sound=20decidable=20type=20equality?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Idris 2 ABI never typechecked. Fixes: - `module Types` only resolves when checked from its own directory; added a minimal `phronesis-abi.ipkg` (no deps; `idris2 --typecheck phronesis-abi.ipkg`) so it has a defined source root and is CI-checkable. - `decEqTy` punted ALL compound types (TyList/TyTuple/TyMap/TyFun) to a wildcard catch-all `decEqTy _ _ = No (\case Refl impossible)`, which is UNSOUND (`TyList a = TyList b` is inhabited by Refl when a = b) and which Idris rejects under `%default total`. Rewritten: compound heads decided structurally via constructor injectivity, mutually with a new field-list decider `decEqTys` (for TyTuple/TyFun); the distinct-head off-diagonal pairs are enumerated (Idris will not accept `Refl impossible` under a wildcard `_ _`). - Removed two unfinished holes about RUNTIME PRIMITIVES that the object logic cannot prove without `believe_me`: `widenPreservesSign` (Int→Double cast sign; its type was also malformed — `Bool` in a `Type` position) and `addCommInt` (Int commutativity). They are not part of the type-safety core; removing them keeps the module total and escape-hatch-free. `idris2 --typecheck phronesis-abi.ipkg` exits 0 under `%default total`: no holes, no `believe_me`/`assert_*`/postulates. The type-safety content — intrinsic `Value : PhroTy -> Type`, total+sound `decEqTy`/`decEqTys`, `widen`, `addSafe` — genuinely checks. SPDX header unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) --- src/abi/Types.idr | 115 ++++++++++++++++++++++++++++++++----- src/abi/phronesis-abi.ipkg | 8 +++ 2 files changed, 108 insertions(+), 15 deletions(-) create mode 100644 src/abi/phronesis-abi.ipkg diff --git a/src/abi/Types.idr b/src/abi/Types.idr index ce27836..c0d099a 100644 --- a/src/abi/Types.idr +++ b/src/abi/Types.idr @@ -31,7 +31,17 @@ data Value : PhroTy -> Type where VList : List (Value t) -> Value (TyList t) VUnit : Value TyUnit --- | Type equality is decidable +-- | Type equality is decidable. +-- +-- Compound types (TyList, TyTuple, TyMap, TyFun) are decided structurally, +-- mutually with the field-list decider `decEqTys`. Every same-head case is +-- handled explicitly, so the final catch-all sees only distinct-head pairs and +-- `Refl impossible` is genuinely valid there. (The earlier version punted ALL +-- compound cases to that catch-all, which is unsound: `TyList a = TyList b` is +-- inhabited by `Refl` when `a = b`.) +public export +decEqTys : (xs, ys : List PhroTy) -> Dec (xs = ys) + public export decEqTy : (t1, t2 : PhroTy) -> Dec (t1 = t2) decEqTy TyInt TyInt = Yes Refl @@ -70,8 +80,95 @@ decEqTy TyUnit TyFloat = No (\case Refl impossible) decEqTy TyUnit TyString = No (\case Refl impossible) decEqTy TyUnit TyBool = No (\case Refl impossible) decEqTy TyUnit TyAtom = No (\case Refl impossible) --- Recursive cases deferred for compound types -decEqTy _ _ = No (\case Refl impossible) +-- recursive (compound) diagonal cases, via constructor injectivity +decEqTy (TyList a) (TyList b) = case decEqTy a b of + Yes Refl => Yes Refl + No contra => No (\case Refl => contra Refl) +decEqTy (TyTuple xs) (TyTuple ys) = case decEqTys xs ys of + Yes Refl => Yes Refl + No contra => No (\case Refl => contra Refl) +decEqTy (TyMap a b) (TyMap c d) = case decEqTy a c of + Yes Refl => case decEqTy b d of + Yes Refl => Yes Refl + No contra => No (\case Refl => contra Refl) + No contra => No (\case Refl => contra Refl) +decEqTy (TyFun args1 ret1) (TyFun args2 ret2) = case decEqTys args1 args2 of + Yes Refl => case decEqTy ret1 ret2 of + Yes Refl => Yes Refl + No contra => No (\case Refl => contra Refl) + No contra => No (\case Refl => contra Refl) +-- remaining off-diagonal pairs involving a compound head (all distinct heads, +-- hence genuinely absurd). Enumerated because Idris will not accept `Refl +-- impossible` under a wildcard `_ _` catch-all. +decEqTy TyInt (TyList _) = No (\case Refl impossible) +decEqTy TyInt (TyTuple _) = No (\case Refl impossible) +decEqTy TyInt (TyMap _ _) = No (\case Refl impossible) +decEqTy TyInt (TyFun _ _) = No (\case Refl impossible) +decEqTy TyFloat (TyList _) = No (\case Refl impossible) +decEqTy TyFloat (TyTuple _) = No (\case Refl impossible) +decEqTy TyFloat (TyMap _ _) = No (\case Refl impossible) +decEqTy TyFloat (TyFun _ _) = No (\case Refl impossible) +decEqTy TyString (TyList _) = No (\case Refl impossible) +decEqTy TyString (TyTuple _) = No (\case Refl impossible) +decEqTy TyString (TyMap _ _) = No (\case Refl impossible) +decEqTy TyString (TyFun _ _) = No (\case Refl impossible) +decEqTy TyBool (TyList _) = No (\case Refl impossible) +decEqTy TyBool (TyTuple _) = No (\case Refl impossible) +decEqTy TyBool (TyMap _ _) = No (\case Refl impossible) +decEqTy TyBool (TyFun _ _) = No (\case Refl impossible) +decEqTy TyAtom (TyList _) = No (\case Refl impossible) +decEqTy TyAtom (TyTuple _) = No (\case Refl impossible) +decEqTy TyAtom (TyMap _ _) = No (\case Refl impossible) +decEqTy TyAtom (TyFun _ _) = No (\case Refl impossible) +decEqTy TyUnit (TyList _) = No (\case Refl impossible) +decEqTy TyUnit (TyTuple _) = No (\case Refl impossible) +decEqTy TyUnit (TyMap _ _) = No (\case Refl impossible) +decEqTy TyUnit (TyFun _ _) = No (\case Refl impossible) +decEqTy (TyList _) TyInt = No (\case Refl impossible) +decEqTy (TyList _) TyFloat = No (\case Refl impossible) +decEqTy (TyList _) TyString = No (\case Refl impossible) +decEqTy (TyList _) TyBool = No (\case Refl impossible) +decEqTy (TyList _) TyAtom = No (\case Refl impossible) +decEqTy (TyList _) TyUnit = No (\case Refl impossible) +decEqTy (TyList _) (TyTuple _) = No (\case Refl impossible) +decEqTy (TyList _) (TyMap _ _) = No (\case Refl impossible) +decEqTy (TyList _) (TyFun _ _) = No (\case Refl impossible) +decEqTy (TyTuple _) TyInt = No (\case Refl impossible) +decEqTy (TyTuple _) TyFloat = No (\case Refl impossible) +decEqTy (TyTuple _) TyString = No (\case Refl impossible) +decEqTy (TyTuple _) TyBool = No (\case Refl impossible) +decEqTy (TyTuple _) TyAtom = No (\case Refl impossible) +decEqTy (TyTuple _) TyUnit = No (\case Refl impossible) +decEqTy (TyTuple _) (TyList _) = No (\case Refl impossible) +decEqTy (TyTuple _) (TyMap _ _) = No (\case Refl impossible) +decEqTy (TyTuple _) (TyFun _ _) = No (\case Refl impossible) +decEqTy (TyMap _ _) TyInt = No (\case Refl impossible) +decEqTy (TyMap _ _) TyFloat = No (\case Refl impossible) +decEqTy (TyMap _ _) TyString = No (\case Refl impossible) +decEqTy (TyMap _ _) TyBool = No (\case Refl impossible) +decEqTy (TyMap _ _) TyAtom = No (\case Refl impossible) +decEqTy (TyMap _ _) TyUnit = No (\case Refl impossible) +decEqTy (TyMap _ _) (TyList _) = No (\case Refl impossible) +decEqTy (TyMap _ _) (TyTuple _) = No (\case Refl impossible) +decEqTy (TyMap _ _) (TyFun _ _) = No (\case Refl impossible) +decEqTy (TyFun _ _) TyInt = No (\case Refl impossible) +decEqTy (TyFun _ _) TyFloat = No (\case Refl impossible) +decEqTy (TyFun _ _) TyString = No (\case Refl impossible) +decEqTy (TyFun _ _) TyBool = No (\case Refl impossible) +decEqTy (TyFun _ _) TyAtom = No (\case Refl impossible) +decEqTy (TyFun _ _) TyUnit = No (\case Refl impossible) +decEqTy (TyFun _ _) (TyList _) = No (\case Refl impossible) +decEqTy (TyFun _ _) (TyTuple _) = No (\case Refl impossible) +decEqTy (TyFun _ _) (TyMap _ _) = No (\case Refl impossible) + +decEqTys [] [] = Yes Refl +decEqTys [] (_ :: _) = No (\case Refl impossible) +decEqTys (_ :: _) [] = No (\case Refl impossible) +decEqTys (x :: xs) (y :: ys) = case decEqTy x y of + Yes Refl => case decEqTys xs ys of + Yes Refl => Yes Refl + No contra => No (\case Refl => contra Refl) + No contra => No (\case Refl => contra Refl) -- | Numeric type predicate public export @@ -84,20 +181,8 @@ public export widen : Value TyInt -> Value TyFloat widen (VInt n) = VFloat (cast n) --- | Widening preserves value (cast is injective for integers in range) -public export -widenPreservesSign : (v : Value TyInt) -> case v of - VInt n => case widen v of - VFloat f => if n >= 0 then f >= 0.0 else f < 0.0 -widenPreservesSign (VInt n) = ?widenPreservesSign_rhs - -- | Type safety: well-typed addition produces well-typed result public export addSafe : IsNumeric t -> Value t -> Value t -> Value t addSafe IntIsNumeric (VInt a) (VInt b) = VInt (a + b) addSafe FloatIsNumeric (VFloat a) (VFloat b) = VFloat (a + b) - --- | Addition is commutative for integers -public export -addCommInt : (a, b : Int) -> a + b = b + a -addCommInt a b = ?addCommInt_rhs -- relies on Int primitives diff --git a/src/abi/phronesis-abi.ipkg b/src/abi/phronesis-abi.ipkg new file mode 100644 index 0000000..a82a9e3 --- /dev/null +++ b/src/abi/phronesis-abi.ipkg @@ -0,0 +1,8 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- Minimal Idris 2 package for the Phronesis ABI type-safety module. +-- No external dependencies (Prelude + base only). Check with: +-- idris2 --typecheck phronesis-abi.ipkg +package phronesis-abi +sourcedir = "." +modules = Types