Skip to content

Commit b0199a9

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
fix(abi/idris): make Types.idr typecheck total — sound decidable type equality (#50)
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) <noreply@anthropic.com>
1 parent 238af47 commit b0199a9

2 files changed

Lines changed: 108 additions & 15 deletions

File tree

‎src/abi/Types.idr‎

Lines changed: 100 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,17 @@ data Value : PhroTy -> Type where
3131
VList : List (Value t) -> Value (TyList t)
3232
VUnit : Value TyUnit
3333

34-
-- | Type equality is decidable
34+
-- | Type equality is decidable.
35+
--
36+
-- Compound types (TyList, TyTuple, TyMap, TyFun) are decided structurally,
37+
-- mutually with the field-list decider `decEqTys`. Every same-head case is
38+
-- handled explicitly, so the final catch-all sees only distinct-head pairs and
39+
-- `Refl impossible` is genuinely valid there. (The earlier version punted ALL
40+
-- compound cases to that catch-all, which is unsound: `TyList a = TyList b` is
41+
-- inhabited by `Refl` when `a = b`.)
42+
public export
43+
decEqTys : (xs, ys : List PhroTy) -> Dec (xs = ys)
44+
3545
public export
3646
decEqTy : (t1, t2 : PhroTy) -> Dec (t1 = t2)
3747
decEqTy TyInt TyInt = Yes Refl
@@ -70,8 +80,95 @@ decEqTy TyUnit TyFloat = No (\case Refl impossible)
7080
decEqTy TyUnit TyString = No (\case Refl impossible)
7181
decEqTy TyUnit TyBool = No (\case Refl impossible)
7282
decEqTy TyUnit TyAtom = No (\case Refl impossible)
73-
-- Recursive cases deferred for compound types
74-
decEqTy _ _ = No (\case Refl impossible)
83+
-- recursive (compound) diagonal cases, via constructor injectivity
84+
decEqTy (TyList a) (TyList b) = case decEqTy a b of
85+
Yes Refl => Yes Refl
86+
No contra => No (\case Refl => contra Refl)
87+
decEqTy (TyTuple xs) (TyTuple ys) = case decEqTys xs ys of
88+
Yes Refl => Yes Refl
89+
No contra => No (\case Refl => contra Refl)
90+
decEqTy (TyMap a b) (TyMap c d) = case decEqTy a c of
91+
Yes Refl => case decEqTy b d of
92+
Yes Refl => Yes Refl
93+
No contra => No (\case Refl => contra Refl)
94+
No contra => No (\case Refl => contra Refl)
95+
decEqTy (TyFun args1 ret1) (TyFun args2 ret2) = case decEqTys args1 args2 of
96+
Yes Refl => case decEqTy ret1 ret2 of
97+
Yes Refl => Yes Refl
98+
No contra => No (\case Refl => contra Refl)
99+
No contra => No (\case Refl => contra Refl)
100+
-- remaining off-diagonal pairs involving a compound head (all distinct heads,
101+
-- hence genuinely absurd). Enumerated because Idris will not accept `Refl
102+
-- impossible` under a wildcard `_ _` catch-all.
103+
decEqTy TyInt (TyList _) = No (\case Refl impossible)
104+
decEqTy TyInt (TyTuple _) = No (\case Refl impossible)
105+
decEqTy TyInt (TyMap _ _) = No (\case Refl impossible)
106+
decEqTy TyInt (TyFun _ _) = No (\case Refl impossible)
107+
decEqTy TyFloat (TyList _) = No (\case Refl impossible)
108+
decEqTy TyFloat (TyTuple _) = No (\case Refl impossible)
109+
decEqTy TyFloat (TyMap _ _) = No (\case Refl impossible)
110+
decEqTy TyFloat (TyFun _ _) = No (\case Refl impossible)
111+
decEqTy TyString (TyList _) = No (\case Refl impossible)
112+
decEqTy TyString (TyTuple _) = No (\case Refl impossible)
113+
decEqTy TyString (TyMap _ _) = No (\case Refl impossible)
114+
decEqTy TyString (TyFun _ _) = No (\case Refl impossible)
115+
decEqTy TyBool (TyList _) = No (\case Refl impossible)
116+
decEqTy TyBool (TyTuple _) = No (\case Refl impossible)
117+
decEqTy TyBool (TyMap _ _) = No (\case Refl impossible)
118+
decEqTy TyBool (TyFun _ _) = No (\case Refl impossible)
119+
decEqTy TyAtom (TyList _) = No (\case Refl impossible)
120+
decEqTy TyAtom (TyTuple _) = No (\case Refl impossible)
121+
decEqTy TyAtom (TyMap _ _) = No (\case Refl impossible)
122+
decEqTy TyAtom (TyFun _ _) = No (\case Refl impossible)
123+
decEqTy TyUnit (TyList _) = No (\case Refl impossible)
124+
decEqTy TyUnit (TyTuple _) = No (\case Refl impossible)
125+
decEqTy TyUnit (TyMap _ _) = No (\case Refl impossible)
126+
decEqTy TyUnit (TyFun _ _) = No (\case Refl impossible)
127+
decEqTy (TyList _) TyInt = No (\case Refl impossible)
128+
decEqTy (TyList _) TyFloat = No (\case Refl impossible)
129+
decEqTy (TyList _) TyString = No (\case Refl impossible)
130+
decEqTy (TyList _) TyBool = No (\case Refl impossible)
131+
decEqTy (TyList _) TyAtom = No (\case Refl impossible)
132+
decEqTy (TyList _) TyUnit = No (\case Refl impossible)
133+
decEqTy (TyList _) (TyTuple _) = No (\case Refl impossible)
134+
decEqTy (TyList _) (TyMap _ _) = No (\case Refl impossible)
135+
decEqTy (TyList _) (TyFun _ _) = No (\case Refl impossible)
136+
decEqTy (TyTuple _) TyInt = No (\case Refl impossible)
137+
decEqTy (TyTuple _) TyFloat = No (\case Refl impossible)
138+
decEqTy (TyTuple _) TyString = No (\case Refl impossible)
139+
decEqTy (TyTuple _) TyBool = No (\case Refl impossible)
140+
decEqTy (TyTuple _) TyAtom = No (\case Refl impossible)
141+
decEqTy (TyTuple _) TyUnit = No (\case Refl impossible)
142+
decEqTy (TyTuple _) (TyList _) = No (\case Refl impossible)
143+
decEqTy (TyTuple _) (TyMap _ _) = No (\case Refl impossible)
144+
decEqTy (TyTuple _) (TyFun _ _) = No (\case Refl impossible)
145+
decEqTy (TyMap _ _) TyInt = No (\case Refl impossible)
146+
decEqTy (TyMap _ _) TyFloat = No (\case Refl impossible)
147+
decEqTy (TyMap _ _) TyString = No (\case Refl impossible)
148+
decEqTy (TyMap _ _) TyBool = No (\case Refl impossible)
149+
decEqTy (TyMap _ _) TyAtom = No (\case Refl impossible)
150+
decEqTy (TyMap _ _) TyUnit = No (\case Refl impossible)
151+
decEqTy (TyMap _ _) (TyList _) = No (\case Refl impossible)
152+
decEqTy (TyMap _ _) (TyTuple _) = No (\case Refl impossible)
153+
decEqTy (TyMap _ _) (TyFun _ _) = No (\case Refl impossible)
154+
decEqTy (TyFun _ _) TyInt = No (\case Refl impossible)
155+
decEqTy (TyFun _ _) TyFloat = No (\case Refl impossible)
156+
decEqTy (TyFun _ _) TyString = No (\case Refl impossible)
157+
decEqTy (TyFun _ _) TyBool = No (\case Refl impossible)
158+
decEqTy (TyFun _ _) TyAtom = No (\case Refl impossible)
159+
decEqTy (TyFun _ _) TyUnit = No (\case Refl impossible)
160+
decEqTy (TyFun _ _) (TyList _) = No (\case Refl impossible)
161+
decEqTy (TyFun _ _) (TyTuple _) = No (\case Refl impossible)
162+
decEqTy (TyFun _ _) (TyMap _ _) = No (\case Refl impossible)
163+
164+
decEqTys [] [] = Yes Refl
165+
decEqTys [] (_ :: _) = No (\case Refl impossible)
166+
decEqTys (_ :: _) [] = No (\case Refl impossible)
167+
decEqTys (x :: xs) (y :: ys) = case decEqTy x y of
168+
Yes Refl => case decEqTys xs ys of
169+
Yes Refl => Yes Refl
170+
No contra => No (\case Refl => contra Refl)
171+
No contra => No (\case Refl => contra Refl)
75172

76173
-- | Numeric type predicate
77174
public export
@@ -84,20 +181,8 @@ public export
84181
widen : Value TyInt -> Value TyFloat
85182
widen (VInt n) = VFloat (cast n)
86183

87-
-- | Widening preserves value (cast is injective for integers in range)
88-
public export
89-
widenPreservesSign : (v : Value TyInt) -> case v of
90-
VInt n => case widen v of
91-
VFloat f => if n >= 0 then f >= 0.0 else f < 0.0
92-
widenPreservesSign (VInt n) = ?widenPreservesSign_rhs
93-
94184
-- | Type safety: well-typed addition produces well-typed result
95185
public export
96186
addSafe : IsNumeric t -> Value t -> Value t -> Value t
97187
addSafe IntIsNumeric (VInt a) (VInt b) = VInt (a + b)
98188
addSafe FloatIsNumeric (VFloat a) (VFloat b) = VFloat (a + b)
99-
100-
-- | Addition is commutative for integers
101-
public export
102-
addCommInt : (a, b : Int) -> a + b = b + a
103-
addCommInt a b = ?addCommInt_rhs -- relies on Int primitives

‎src/abi/phronesis-abi.ipkg‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
-- Minimal Idris 2 package for the Phronesis ABI type-safety module.
4+
-- No external dependencies (Prelude + base only). Check with:
5+
-- idris2 --typecheck phronesis-abi.ipkg
6+
package phronesis-abi
7+
sourcedir = "."
8+
modules = Types

0 commit comments

Comments
 (0)