Merge branch 'master' into merge

docs/_pages/library.md

@@ -466,6 +466,13 @@ function table.isfrozen(t: table): boolean
 
 Returns `true` iff the input table is frozen.
 
+```
+function table.clone(t: table): table
+```
+
+Returns a copy of the input table that has the same metatable, same keys and values, and is not frozen even if `t` was.
+The copy is shallow: implementing a deep recursive copy automatically is challenging, and often only certain keys need to be cloned recursively which can be done after the initial clone by modifying the resulting table.
+
 ## string library
 
 ```

prototyping/FFI/Data/Aeson.agda

@@ -10,7 +10,7 @@ open import Agda.Builtin.String using (String)
 open import FFI.Data.ByteString using (ByteString)
 open import FFI.Data.HaskellString using (HaskellString; pack)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
-open import FFI.Data.Either using (Either; mapLeft)
+open import FFI.Data.Either using (Either; mapL)
 open import FFI.Data.Scientific using (Scientific)
 open import FFI.Data.Vector using (Vector)
 
@@ -73,5 +73,5 @@ postulate
 {-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-}
 
 eitherDecode : ByteString → Either String Value
-eitherDecode bytes = mapLeft pack (eitherHDecode bytes)
+eitherDecode bytes = mapL pack (eitherHDecode bytes)
 

prototyping/FFI/Data/Either.agda

@@ -7,10 +7,22 @@ data Either (A B : Set) : Set where
   Right : B → Either A B
 {-# COMPILE GHC Either = data Data.Either.Either (Data.Either.Left|Data.Either.Right) #-}
 
-mapLeft : ∀ {A B C} → (A → B) → (Either A C) → (Either B C)
-mapLeft f (Left x) = Left (f x)
-mapLeft f (Right x) = Right x
+swapLR : ∀ {A B} → Either A B → Either B A
+swapLR (Left x) = Right x
+swapLR (Right x) = Left x
 
-mapRight : ∀ {A B C} → (B → C) → (Either A B) → (Either A C)
-mapRight f (Left x) = Left x
-mapRight f (Right x) = Right (f x)
+mapL : ∀ {A B C} → (A → B) → Either A C → Either B C
+mapL f (Left x) = Left (f x)
+mapL f (Right x) = Right x
+
+mapR : ∀ {A B C} → (B → C) → Either A B → Either A C
+mapR f (Left x) = Left x
+mapR f (Right x) = Right (f x)
+
+mapLR : ∀ {A B C D} → (A → B) → (C → D) → Either A C → Either B D
+mapLR f g (Left x) = Left (f x)
+mapLR f g (Right x) = Right (g x)
+
+cond : ∀ {A B C : Set} → (A → C) → (B → C) → (Either A B) → C
+cond f g (Left x) = f x
+cond f g (Right x) = g x

prototyping/Luau/RuntimeError.agda

@@ -25,7 +25,7 @@ data RuntimeErrorᴮ {a} (H : Heap a) : Block a → Set
 data RuntimeErrorᴱ {a} (H : Heap a) : Expr a → Set
 
 data RuntimeErrorᴱ H where
-  FunctionMismatch : ∀ v w → (function ≢ valueType v) → RuntimeErrorᴱ H (val v $ val w)
+  FunctionMismatch : ∀ v w → (valueType v ≢ function) → RuntimeErrorᴱ H (val v $ val w)
   BinOpMismatch₁ : ∀ v w {op} → (BinOpError op (valueType v)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
   BinOpMismatch₂ : ∀ v w {op} → (BinOpError op (valueType w)) → RuntimeErrorᴱ H (binexp (val v) op (val w))
   UnboundVariable : ∀ {x} → RuntimeErrorᴱ H (var x)

prototyping/Luau/StrictMode.agda

@@ -5,28 +5,18 @@ module Luau.StrictMode where
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.Type using (Type; strict; nil; number; string; _⇒_; tgt)
+open import Luau.Type using (Type; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt)
+open import Luau.Subtyping using (_≮:_)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
-open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function)
-open import Properties.Equality using (_≢_)
+open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; ⊢ᴴ_; ⊢ᴼ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; var; addr; app; binexp; block; return; local; function; srcBinOp)
+open import Properties.Contradiction using (¬)
 open import Properties.TypeCheck(strict) using (typeCheckᴮ)
 open import Properties.Product using (_,_)
 
 src : Type → Type
 src = Luau.Type.src strict
 
-data BinOpWarning : BinaryOperator → Type → Set where
-  + : ∀ {T} → (T ≢ number) → BinOpWarning + T
-  - : ∀ {T} → (T ≢ number) → BinOpWarning - T
-  * : ∀ {T} → (T ≢ number) → BinOpWarning * T
-  / : ∀ {T} → (T ≢ number) → BinOpWarning / T
-  < : ∀ {T} → (T ≢ number) → BinOpWarning < T
-  > : ∀ {T} → (T ≢ number) → BinOpWarning > T
-  <= : ∀ {T} → (T ≢ number) → BinOpWarning <= T
-  >= : ∀ {T} → (T ≢ number) → BinOpWarning >= T
-  ·· : ∀ {T} → (T ≢ string) → BinOpWarning ·· T
-
 data Warningᴱ (H : Heap yes) {Γ} : ∀ {M T} → (Γ ⊢ᴱ M ∈ T) → Set
 data Warningᴮ (H : Heap yes) {Γ} : ∀ {B T} → (Γ ⊢ᴮ B ∈ T) → Set
 
@@ -46,7 +36,7 @@ data Warningᴱ H {Γ} where
 
   FunctionCallMismatch : ∀ {M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
 
-    (src T ≢ U) →
+    (U ≮: src T) →
     -----------------
     Warningᴱ H (app D₁ D₂)
   
@@ -64,13 +54,13 @@ data Warningᴱ H {Γ} where
 
   BinOpMismatch₁ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
 
-    BinOpWarning op T →
+    (T ≮: srcBinOp op) →
     ------------------------------
     Warningᴱ H (binexp {op} D₁ D₂)
 
   BinOpMismatch₂ : ∀ {op M N T U} {D₁ : Γ ⊢ᴱ M ∈ T} {D₂ : Γ ⊢ᴱ N ∈ U} →
 
-    BinOpWarning op U →
+    (U ≮: srcBinOp op) →
     ------------------------------
     Warningᴱ H (binexp {op} D₁ D₂)
 
@@ -88,7 +78,7 @@ data Warningᴱ H {Γ} where
     
   FunctionDefnMismatch : ∀ {f x B T U V} {D : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
 
-    (U ≢ V) →
+    (V ≮: U) →
     -------------------------
     Warningᴱ H (function {f} {U = U} D)
 
@@ -100,7 +90,7 @@ data Warningᴱ H {Γ} where
 
   BlockMismatch : ∀ {b B T U} {D : Γ ⊢ᴮ B ∈ U} →
 
-    (T ≢ U) →
+    (U ≮: T) →
     ------------------------------
     Warningᴱ H (block {b} {T = T} D)
 
@@ -120,7 +110,7 @@ data Warningᴮ H {Γ} where
 
   LocalVarMismatch : ∀ {x M B T U V} {D₁ : Γ ⊢ᴱ M ∈ U} {D₂ : (Γ ⊕ x ↦ T) ⊢ᴮ B ∈ V} →
 
-    (T ≢ U) →
+    (U ≮: T) →
     --------------------
     Warningᴮ H (local D₁ D₂)
 
@@ -138,7 +128,7 @@ data Warningᴮ H {Γ} where
 
   FunctionDefnMismatch : ∀ {f x B C T U V W} {D₁ : (Γ ⊕ x ↦ T) ⊢ᴮ C ∈ V} {D₂ : (Γ ⊕ f ↦ (T ⇒ U)) ⊢ᴮ B ∈ W} →
 
-    (U ≢ V) →
+    (V ≮: U) →
     -------------------------------------
     Warningᴮ H (function D₁ D₂)
 
@@ -158,7 +148,7 @@ data Warningᴼ (H : Heap yes) : ∀ {V} → (⊢ᴼ V) → Set where
 
   FunctionDefnMismatch : ∀ {f x B T U V} {D : (x ↦ T) ⊢ᴮ B ∈ V} →
 
-    (U ≢ V) →
+    (V ≮: U) →
     ---------------------------------
     Warningᴼ H (function {f} {U = U} D)
 

prototyping/Luau/StrictMode/ToString.agda

@@ -2,37 +2,58 @@
 
 module Luau.StrictMode.ToString where
 
+open import Agda.Builtin.Nat using (Nat; suc)
 open import FFI.Data.String using (String; _++_)
+open import Luau.Subtyping using (_≮:_; Tree; witness; scalar; function; function-ok; function-err)
 open import Luau.StrictMode using (Warningᴱ; Warningᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; FunctionDefnMismatch; BlockMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; block₁; return; LocalVarMismatch; local₁; local₂; function₁; function₂; heap; expr; block; addr)
 open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; number; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
-open import Luau.Type using (strict)
+open import Luau.Type using (strict; number; boolean; string; nil)
 open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_)
 open import Luau.Addr.ToString using (addrToString)
 open import Luau.Var.ToString using (varToString)
 open import Luau.Type.ToString using (typeToString)
 open import Luau.Syntax.ToString using (binOpToString)
 
+tmp : Nat → String
+tmp 0 = "w"
+tmp 1 = "x"
+tmp 2 = "y"
+tmp 3 = "z"
+tmp (suc (suc (suc n))) = tmp n ++ "'"
+
+treeToString : Tree → Nat → String → String
+treeToString (scalar number) n v = v ++ " is a number"
+treeToString (scalar boolean) n v = v ++ " is a boolean"
+treeToString (scalar string) n v = v ++ " is a string"
+treeToString (scalar nil) n v = v ++ " is nil"
+treeToString function n v = v ++ " is a function"
+treeToString (function-ok t) n v = treeToString t n (v ++ "()")
+treeToString (function-err t) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ treeToString t (suc n) w where w = tmp n
+
+subtypeWarningToString : ∀ {T U} → (T ≮: U) → String
+subtypeWarningToString (witness t p q) = "\n  because provided type contains v, where " ++ treeToString t 0 "v"
+
 warningToStringᴱ : ∀ {H Γ T} M → {D : Γ ⊢ᴱ M ∈ T} → Warningᴱ H D → String
 warningToStringᴮ : ∀ {H Γ T} B → {D : Γ ⊢ᴮ B ∈ T} → Warningᴮ H D → String
 
 warningToStringᴱ (var x) (UnboundVariable p) = "Unbound variable " ++ varToString x
-warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated adress " ++ addrToString a
-warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U
+warningToStringᴱ (val (addr a)) (UnallocatedAddress p) = "Unallocated address " ++ addrToString a
+warningToStringᴱ (M $ N) (FunctionCallMismatch {T = T} {U = U} p) = "Function has type " ++ typeToString T ++ " but argument has type " ++ typeToString U ++ subtypeWarningToString p
 warningToStringᴱ (M $ N) (app₁ W) = warningToStringᴱ M W
 warningToStringᴱ (M $ N) (app₂ W) = warningToStringᴱ N W
-warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
+warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (FunctionDefnMismatch {V = V} p) = "Function expresion " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p
 warningToStringᴱ (function f ⟨ var x ∈ T ⟩∈ U is B end) (function₁ W) = warningToStringᴮ B W ++ "\n  in function expression " ++ varToString f
-warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) =  "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U
+warningToStringᴱ block var b ∈ T is B end (BlockMismatch {U = U} p) =  "Block " ++ varToString b ++ " has type " ++ typeToString T ++ " but body returns " ++ typeToString U ++ subtypeWarningToString p
 warningToStringᴱ block var b ∈ T is B end (block₁ W) = warningToStringᴮ B W ++ "\n  in block " ++ varToString b
-warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T 
-warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U
+warningToStringᴱ (binexp M op N) (BinOpMismatch₁ {T = T} p) = "Binary operator " ++ binOpToString op ++ " lhs has type " ++ typeToString T ++ subtypeWarningToString p
+warningToStringᴱ (binexp M op N) (BinOpMismatch₂ {U = U} p) = "Binary operator " ++ binOpToString op ++ " rhs has type " ++ typeToString U ++ subtypeWarningToString p
 warningToStringᴱ (binexp M op N) (bin₁ W) = warningToStringᴱ M W
 warningToStringᴱ (binexp M op N) (bin₂ W) = warningToStringᴱ N W
 
-warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V
+warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (FunctionDefnMismatch {V = V} p) = "Function declaration " ++ varToString f ++ " has return type " ++ typeToString U ++ " but body returns " ++ typeToString V ++ subtypeWarningToString p
 warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₁ W) = warningToStringᴮ C W ++ "\n  in function declaration " ++ varToString f
 warningToStringᴮ (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function₂ W) = warningToStringᴮ B W
-warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) =  "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U
+warningToStringᴮ (local var x ∈ T ← M ∙ B) (LocalVarMismatch {U = U} p) =  "Local variable " ++ varToString x ++ " has type " ++ typeToString T ++ " but expression has type " ++ typeToString U ++ subtypeWarningToString p
 warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₁ W) = warningToStringᴱ M W ++ "\n  in local variable declaration " ++ varToString x
 warningToStringᴮ (local var x ∈ T ← M ∙ B) (local₂ W) = warningToStringᴮ B W
 warningToStringᴮ (return M ∙ B) (return W) = warningToStringᴱ M W ++ "\n  in return statement"

prototyping/Luau/Subtyping.agda

@@ -0,0 +1,62 @@
+{-# OPTIONS --rewriting #-}
+
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_)
+open import Properties.Equality using (_≢_)
+
+module Luau.Subtyping where
+
+-- An implementation of semantic subtyping
+
+-- We think of types as languages of trees
+
+data Tree : Set where
+
+  scalar : ∀ {T} → Scalar T → Tree
+  function : Tree
+  function-ok : Tree → Tree
+  function-err : Tree → Tree
+
+data Language : Type → Tree → Set
+data ¬Language : Type → Tree → Set
+
+data Language where
+
+  scalar : ∀ {T} → (s : Scalar T) → Language T (scalar s)
+  function : ∀ {T U} → Language (T ⇒ U) function
+  function-ok : ∀ {T U u} → (Language U u) → Language (T ⇒ U) (function-ok u)
+  function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
+  scalar-function-err : ∀ {S t} → (Scalar S) → Language S (function-err t)
+  left : ∀ {T U t} → Language T t → Language (T ∪ U) t
+  right : ∀ {T U u} → Language U u → Language (T ∪ U) u
+  _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
+  any : ∀ {t} → Language any t
+
+data ¬Language where
+
+  scalar-scalar : ∀ {S T} → (s : Scalar S) → (Scalar T) → (S ≢ T) → ¬Language T (scalar s)
+  scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
+  scalar-function-ok : ∀ {S u} → (Scalar S) → ¬Language S (function-ok u)
+  function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
+  function-ok : ∀ {T U u} → (¬Language U u) → ¬Language (T ⇒ U) (function-ok u)
+  function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
+  _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
+  left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
+  right : ∀ {T U u} → ¬Language U u → ¬Language (T ∩ U) u
+  none : ∀ {t} → ¬Language none t
+
+-- Subtyping as language inclusion
+
+_<:_ : Type → Type → Set
+(T <: U) = ∀ t → (Language T t) → (Language U t)
+
+-- For warnings, we are interested in failures of subtyping,
+-- which is whrn there is a tree in T's language that isn't in U's.
+
+data _≮:_ (T U : Type) : Set where
+
+  witness : ∀ t →
+
+    Language T t →
+    ¬Language U t →
+    -----------------
+    T ≮: U

prototyping/Luau/Type.agda

@@ -17,6 +17,13 @@ data Type : Set where
   _∪_ : Type → Type → Type
   _∩_ : Type → Type → Type
 
+data Scalar : Type → Set where
+
+  number : Scalar number
+  boolean : Scalar boolean
+  string : Scalar string
+  nil : Scalar nil
+
 lhs : Type → Type
 lhs (T ⇒ _) = T
 lhs (T ∪ _) = T

prototyping/Luau/TypeCheck.agda

@@ -10,7 +10,7 @@ open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.Type using (Type; Mode; nil; none; number; boolean; string; _⇒_; tgt)
+open import Luau.Type using (Type; Mode; nil; any; number; boolean; string; _⇒_; tgt)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
@@ -19,9 +19,22 @@ open import Properties.Product using (_×_; _,_)
 src : Type → Type
 src = Luau.Type.src m
 
-orNone : Maybe Type → Type
-orNone nothing = none
-orNone (just T) = T
+orAny : Maybe Type → Type
+orAny nothing = any
+orAny (just T) = T
+
+srcBinOp : BinaryOperator → Type
+srcBinOp + = number
+srcBinOp - = number
+srcBinOp * = number
+srcBinOp / = number
+srcBinOp < = number
+srcBinOp > = number
+srcBinOp == = any
+srcBinOp ~= = any
+srcBinOp <= = number
+srcBinOp >= = number
+srcBinOp ·· = string
 
 tgtBinOp : BinaryOperator → Type
 tgtBinOp + = number
@@ -76,7 +89,7 @@ data _⊢ᴱ_∈_ where
 
   var : ∀ {x T Γ} →
 
-    T ≡ orNone(Γ [ x ]ⱽ) →
+    T ≡ orAny(Γ [ x ]ⱽ) →
     ----------------
     Γ ⊢ᴱ (var x) ∈ T
 

prototyping/Properties.agda

@@ -5,7 +5,9 @@ module Properties where
 import Properties.Contradiction
 import Properties.Dec
 import Properties.Equality
+import Properties.Functions
 import Properties.Remember
 import Properties.Step
 import Properties.StrictMode
+import Properties.Subtyping
 import Properties.TypeCheck

prototyping/Properties/Functions.agda

@@ -0,0 +1,6 @@
+module Properties.Functions where
+
+infixr 5 _∘_
+
+_∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
+(f ∘ g) x = f (g x)

prototyping/Properties/StrictMode.agda

@@ -4,13 +4,15 @@ module Properties.StrictMode where
 
 import Agda.Builtin.Equality.Rewrite
 open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import Luau.Heap using (Heap; Object; function_is_end; defn; alloc; ok; next; lookup-not-allocated) renaming (_≡_⊕_↦_ to _≡ᴴ_⊕_↦_; _[_] to _[_]ᴴ; ∅ to ∅ᴴ)
-open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴᴱ; Warningᴴᴮ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpWarning; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr; +; -; *; /; <; >; <=; >=; ··)
+open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warningᴴ; UnallocatedAddress; UnboundVariable; FunctionCallMismatch; app₁; app₂; BinOpMismatch₁; BinOpMismatch₂; bin₁; bin₂; BlockMismatch; block₁; return; LocalVarMismatch; local₁; local₂; FunctionDefnMismatch; function₁; function₂; heap; expr; block; addr)
 open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
+open import Luau.Subtyping using (_≮:_; witness; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language)
 open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
-open import Luau.Type using (Type; strict; nil; _⇒_; none; tgt; _≡ᵀ_; _≡ᴹᵀ_)
-open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orNone; tgtBinOp)
+open import Luau.Type using (Type; strict; nil; number; boolean; string; _⇒_; none; any; _∩_; _∪_; tgt; _≡ᵀ_; _≡ᴹᵀ_)
+open import Luau.TypeCheck(strict) using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orAny; srcBinOp; tgtBinOp)
 open import Luau.Var using (_≡ⱽ_)
 open import Luau.Addr using (_≡ᴬ_)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_; ⊕-lookup-miss; ⊕-swap; ⊕-over) renaming (_[_] to _[_]ⱽ)
@@ -18,17 +20,19 @@ open import Luau.VarCtxt using (VarCtxt; ∅)
 open import Properties.Remember using (remember; _,_)
 open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
 open import Properties.Dec using (Dec; yes; no)
-open import Properties.Contradiction using (CONTRADICTION)
-open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴᴱ; typeCheckᴴᴮ; mustBeFunction; mustBeNumber; mustBeString)
+open import Properties.Contradiction using (CONTRADICTION; ¬)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (any-≮:; ≡-trans-≮:; ≮:-trans-≡; none-tgt-≮:; tgt-none-≮:; src-any-≮:; any-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-none; any-≮:-scalar; scalar-≮:-none; any-≮:-none)
+open import Properties.TypeCheck(strict) using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ)
 open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.RuntimeType using (valueType)
+open import Luau.RuntimeType using (RuntimeType; valueType; number; string; boolean; nil; function)
 
 src = Luau.Type.src strict
 
 data _⊑_ (H : Heap yes) : Heap yes → Set where
   refl : (H ⊑ H)
-  snoc : ∀ {H′ a V} → (H′ ≡ᴴ H ⊕ a ↦ V) → (H ⊑ H′)
+  snoc : ∀ {H′ a O} → (H′ ≡ᴴ H ⊕ a ↦ O) → (H ⊑ H′)
 
 rednᴱ⊑ : ∀ {H H′ M M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (H ⊑ H′)
 rednᴮ⊑ : ∀ {H H′ B B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (H ⊑ H′)
@@ -59,90 +63,51 @@ lookup-⊑-nothing {H} a (snoc defn) p with a ≡ᴬ next H
 lookup-⊑-nothing {H} a (snoc defn) p | yes refl = refl
 lookup-⊑-nothing {H} a (snoc o) p | no q = trans (lookup-not-allocated o q) p
 
-data OrWarningᴱ {Γ M T} (H : Heap yes) (D : Γ ⊢ᴱ M ∈ T) A : Set where
-  ok : A → OrWarningᴱ H D A
-  warning : Warningᴱ H D → OrWarningᴱ H D A
+heap-weakeningᴱ : ∀ Γ H M {H′ U} → (H ⊑ H′) → (typeOfᴱ H′ Γ M ≮: U) → (typeOfᴱ H Γ M ≮: U)
+heap-weakeningᴱ Γ H (var x) h p = p
+heap-weakeningᴱ Γ H (val nil) h p = p
+heap-weakeningᴱ Γ H (val (addr a)) refl p = p
+heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p with a ≡ᴬ b
+heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = a} defn) p | yes refl = any-≮: p
+heap-weakeningᴱ Γ H (val (addr a)) (snoc {a = b} q) p | no r = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ (lookup-not-allocated q r))) p
+heap-weakeningᴱ Γ H (val (number x)) h p = p
+heap-weakeningᴱ Γ H (val (bool x)) h p = p
+heap-weakeningᴱ Γ H (val (string x)) h p = p
+heap-weakeningᴱ Γ H (M $ N) h p = none-tgt-≮: (heap-weakeningᴱ Γ H M h (tgt-none-≮: p))
+heap-weakeningᴱ Γ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h p = p
+heap-weakeningᴱ Γ H (block var b ∈ T is B end) h p = p
+heap-weakeningᴱ Γ H (binexp M op N) h p = p
 
-data OrWarningᴮ {Γ B T} (H : Heap yes) (D : Γ ⊢ᴮ B ∈ T) A : Set where
-  ok : A → OrWarningᴮ H D A
-  warning : Warningᴮ H D → OrWarningᴮ H D A
+heap-weakeningᴮ : ∀ Γ H B {H′ U} → (H ⊑ H′) → (typeOfᴮ H′ Γ B ≮: U) → (typeOfᴮ H Γ B ≮: U)
+heap-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h p = heap-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h p
+heap-weakeningᴮ Γ H (local var x ∈ T ← M ∙ B) h p = heap-weakeningᴮ (Γ ⊕ x ↦ T) H B h p
+heap-weakeningᴮ Γ H (return M ∙ B) h p = heap-weakeningᴱ Γ H M h p
+heap-weakeningᴮ Γ H done h p = p
 
-data OrWarningᴴᴱ {Γ M T} H (D : Γ ⊢ᴴᴱ H ▷ M ∈ T) A : Set where
-  ok : A → OrWarningᴴᴱ H D A
-  warning : Warningᴴᴱ H D → OrWarningᴴᴱ H D A
+substitutivityᴱ : ∀ {Γ T U} H M v x → (typeOfᴱ H Γ (M [ v / x ]ᴱ) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) M ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
+substitutivityᴱ-whenever : ∀ {Γ T U} H v x y (r : Dec(x ≡ y)) → (typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever r) ≮: U) → Either (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
+substitutivityᴮ : ∀ {Γ T U} H B v x → (typeOfᴮ H Γ (B [ v / x ]ᴮ) ≮: U) → Either (typeOfᴮ H (Γ ⊕ x ↦ T) B ≮: U) (typeOfᴱ H ∅ (val v) ≮: T)
+substitutivityᴮ-unless : ∀ {Γ T U V} H B v x y (r : Dec(x ≡ y)) → (typeOfᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r) ≮: V) → Either (typeOfᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
+substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T V} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless yes r) ≮: V) → Either (typeOfᴮ H Γ′ B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
+substitutivityᴮ-unless-no : ∀ {Γ Γ′ T V} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ (B [ v / x ]ᴮunless no r) ≮: V) → Either (typeOfᴮ H Γ′ B ≮: V) (typeOfᴱ H ∅ (val v) ≮: T)
 
-data OrWarningᴴᴮ {Γ B T} H (D : Γ ⊢ᴴᴮ H ▷ B ∈ T) A : Set where
-  ok : A → OrWarningᴴᴮ H D A
-  warning : Warningᴴᴮ H D → OrWarningᴴᴮ H D A
+substitutivityᴱ H (var y) v x p = substitutivityᴱ-whenever H v x y (x ≡ⱽ y) p
+substitutivityᴱ H (val w) v x p = Left p
+substitutivityᴱ H (binexp M op N) v x p = Left p
+substitutivityᴱ H (M $ N) v x p = mapL none-tgt-≮: (substitutivityᴱ H M v x (tgt-none-≮: p))
+substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = Left p
+substitutivityᴱ H (block var b ∈ T is B end) v x p = Left p
+substitutivityᴱ-whenever H v x x (yes refl) q = swapLR (≮:-trans q)
+substitutivityᴱ-whenever H v x y (no p) q = Left (≡-trans-≮: (cong orAny (sym (⊕-lookup-miss x y _ _ p))) q)
 
-heap-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → OrWarningᴱ H (typeCheckᴱ H Γ M) (typeOfᴱ H Γ M ≡ typeOfᴱ H′ Γ M)
-heap-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → OrWarningᴮ H (typeCheckᴮ H Γ B) (typeOfᴮ H Γ B ≡ typeOfᴮ H′ Γ B)
-
-heap-weakeningᴱ H (var x) h = ok refl
-heap-weakeningᴱ H (val nil) h = ok refl
-heap-weakeningᴱ H (val (addr a)) refl = ok refl
-heap-weakeningᴱ H (val (addr a)) (snoc {a = b} defn) with a ≡ᴬ b
-heap-weakeningᴱ H (val (addr a)) (snoc {a = a} defn) | yes refl = warning (UnallocatedAddress refl)
-heap-weakeningᴱ H (val (addr a)) (snoc {a = b} p) | no q = ok (cong orNone (cong typeOfᴹᴼ (lookup-not-allocated p q)))
-heap-weakeningᴱ H (val (number n)) h = ok refl
-heap-weakeningᴱ H (val (bool b)) h = ok refl
-heap-weakeningᴱ H (val (string x)) h = ok refl
-heap-weakeningᴱ H (binexp M op N) h = ok refl
-heap-weakeningᴱ H (M $ N) h with heap-weakeningᴱ H M h
-heap-weakeningᴱ H (M $ N) h | ok p = ok (cong tgt p)
-heap-weakeningᴱ H (M $ N) h | warning W = warning (app₁ W)
-heap-weakeningᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) h = ok refl
-heap-weakeningᴱ H (block var b ∈ T is B end) h = ok refl
-heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h with heap-weakeningᴮ H B h
-heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | ok p = ok p
-heap-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h | warning W = warning (function₂ W)
-heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h with heap-weakeningᴮ H B h
-heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | ok p = ok p
-heap-weakeningᴮ H (local var x ∈ T ← M ∙ B) h | warning W = warning (local₂ W)
-heap-weakeningᴮ H (return M ∙ B) h with heap-weakeningᴱ H M h
-heap-weakeningᴮ H (return M ∙ B) h | ok p = ok p
-heap-weakeningᴮ H (return M ∙ B) h | warning W = warning (return W)
-heap-weakeningᴮ H (done) h = ok refl
-
-none-not-obj : ∀ O → none ≢ typeOfᴼ O
-none-not-obj (function f ⟨ var x ∈ T ⟩∈ U is B end) ()
-
-typeOf-val-not-none : ∀ {H Γ} v → OrWarningᴱ H (typeCheckᴱ H Γ (val v)) (none ≢ typeOfᴱ H Γ (val v))
-typeOf-val-not-none nil = ok (λ ())
-typeOf-val-not-none (number n) = ok (λ ())
-typeOf-val-not-none (bool b) = ok (λ ())
-typeOf-val-not-none (string x) = ok (λ ())
-typeOf-val-not-none {H = H} (addr a) with remember (H [ a ]ᴴ)
-typeOf-val-not-none {H = H} (addr a) | (just O , p) = ok (λ q → none-not-obj O (trans q (cong orNone (cong typeOfᴹᴼ p))))
-typeOf-val-not-none {H = H} (addr a) | (nothing , p) = warning (UnallocatedAddress p)
-
-substitutivityᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) M ≡ typeOfᴱ H Γ (M [ v / x ]ᴱ))
-substitutivityᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (yes p)))
-substitutivityᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (typeOfᴱ H (Γ ⊕ x ↦ T) (var y) ≡ typeOfᴱ H Γ (var y [ v / x ]ᴱwhenever (no p)))
-substitutivityᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → (typeOfᴮ H (Γ ⊕ x ↦ T) B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮ))
-substitutivityᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (yes p)))
-substitutivityᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → (typeOfᴮ H Γ′ B ≡ typeOfᴮ H Γ (B [ v / x ]ᴮunless (no p)))
-
-substitutivityᴱ H (var y) v x p with x ≡ⱽ y
-substitutivityᴱ H (var y) v x p | yes q = substitutivityᴱ-whenever-yes H v x y q p
-substitutivityᴱ H (var y) v x p | no q = substitutivityᴱ-whenever-no H v x y q p
-substitutivityᴱ H (val w) v x p = refl
-substitutivityᴱ H (binexp M op N) v x p = refl
-substitutivityᴱ H (M $ N) v x p = cong tgt (substitutivityᴱ H M v x p)
-substitutivityᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p = refl
-substitutivityᴱ H (block var b ∈ T is B end) v x p = refl
-substitutivityᴱ-whenever-yes H v x x refl q = cong orNone q
-substitutivityᴱ-whenever-no H v x y p q = cong orNone ( sym (⊕-lookup-miss x y _ _ p))
-substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p with x ≡ⱽ f
-substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x f q p (⊕-over q)
-substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p | no q = substitutivityᴮ-unless-no H B v x f q p (⊕-swap q)
-substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p with x ≡ⱽ y
-substitutivityᴮ H (local var y ∈ T  ← M ∙ B) v x p | yes q = substitutivityᴮ-unless-yes H B v x y q p (⊕-over q)
-substitutivityᴮ H (local var y ∈ T  ← M ∙ B) v x p | no q =  substitutivityᴮ-unless-no H B v x y q p (⊕-swap q)
+substitutivityᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p = substitutivityᴮ-unless H B v x f (x ≡ⱽ f) p
+substitutivityᴮ H (local var y ∈ T ← M ∙ B) v x p = substitutivityᴮ-unless H B v x y (x ≡ⱽ y) p
 substitutivityᴮ H (return M ∙ B) v x p = substitutivityᴱ H M v x p
-substitutivityᴮ H done v x p = refl
-substitutivityᴮ-unless-yes H B v x x refl q refl = refl
-substitutivityᴮ-unless-no H B v x y p q refl = substitutivityᴮ H B v x q
+substitutivityᴮ H done v x p = Left p
+substitutivityᴮ-unless H B v x y (yes p) q = substitutivityᴮ-unless-yes H B v x y p (⊕-over p) q
+substitutivityᴮ-unless H B v x y (no p) q = substitutivityᴮ-unless-no H B v x y p (⊕-swap p) q
+substitutivityᴮ-unless-yes H B v x y refl refl p = Left p
+substitutivityᴮ-unless-no H B v x y p refl q = substitutivityᴮ H B v x q
 
 binOpPreservation : ∀ H {op v w x} → (v ⟦ op ⟧ w ⟶ x) → (tgtBinOp op ≡ typeOfᴱ H ∅ (val x))
 binOpPreservation H (+ m n) = refl
@@ -157,306 +122,215 @@ binOpPreservation H (== v w) = refl
 binOpPreservation H (~= v w) = refl
 binOpPreservation H (·· v w) = refl
 
-preservationᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → OrWarningᴴᴱ H (typeCheckᴴᴱ H ∅ M) (typeOfᴱ H ∅ M ≡ typeOfᴱ H′ ∅ M′)
-preservationᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → OrWarningᴴᴮ H (typeCheckᴴᴮ H ∅ B) (typeOfᴮ H ∅ B ≡ typeOfᴮ H′ ∅ B′)
+reflect-subtypingᴱ : ∀ H M {H′ M′ T} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → (typeOfᴱ H′ ∅ M′ ≮: T) → Either (typeOfᴱ H ∅ M ≮: T) (Warningᴱ H (typeCheckᴱ H ∅ M))
+reflect-subtypingᴮ : ∀ H B {H′ B′ T} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → (typeOfᴮ H′ ∅ B′ ≮: T) → Either (typeOfᴮ H ∅ B ≮: T) (Warningᴮ H (typeCheckᴮ H ∅ B))
 
-preservationᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) = ok refl
-preservationᴱ H (M $ N) (app₁ s) with preservationᴱ H M s
-preservationᴱ H (M $ N) (app₁ s) | ok p = ok (cong tgt p)
-preservationᴱ H (M $ N) (app₁ s) | warning (expr W) = warning (expr (app₁ W))
-preservationᴱ H (M $ N) (app₁ s) | warning (heap W) = warning (heap W)
-preservationᴱ H (M $ N) (app₂ p s) with heap-weakeningᴱ H M (rednᴱ⊑ s)
-preservationᴱ H (M $ N) (app₂ p s) | ok q = ok (cong tgt q)
-preservationᴱ H (M $ N) (app₂ p s) | warning W  = warning (expr (app₁ W))
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) with remember (typeOfⱽ H v)
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) with S ≡ᵀ U | T ≡ᵀ typeOfᴮ H (x ↦ S) B
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | yes refl = ok (cong tgt (cong orNone (cong typeOfᴹᴼ p)))
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | yes refl | no r = warning (heap (addr a p (FunctionDefnMismatch r)))
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (just U , q) | no r | _ = warning (expr (FunctionCallMismatch (λ s → r (trans (trans (sym (cong src (cong orNone (cong typeOfᴹᴼ p)))) s) (cong orNone q)))))
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) with typeOf-val-not-none v
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | ok r = CONTRADICTION (r (sym (cong orNone q)))
-preservationᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ S ⟩∈ T is B end) v refl p) | (nothing , q) | warning W = warning (expr (app₂ W))
-preservationᴱ H (block var b ∈ T is B end) (block s) = ok refl
-preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) with T ≡ᵀ typeOfᴱ H ∅ (val v)
-preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | yes p = ok p
-preservationᴱ H (block var b ∈ T is return M ∙ B end) (return v) | no p = warning (expr (BlockMismatch p))
-preservationᴱ H (block var b ∈ T is done end) (done) with T ≡ᵀ nil
-preservationᴱ H (block var b ∈ T is done end) (done) | yes p = ok p
-preservationᴱ H (block var b ∈ T is done end) (done) | no p = warning (expr (BlockMismatch p))
-preservationᴱ H (binexp M op N) (binOp₀ s) = ok (binOpPreservation H s)
-preservationᴱ H (binexp M op N) (binOp₁ s) = ok refl
-preservationᴱ H (binexp M op N) (binOp₂ s) = ok refl
+reflect-subtypingᴱ H (M $ N) (app₁ s) p = mapLR none-tgt-≮: app₁ (reflect-subtypingᴱ H M s (tgt-none-≮: p))
+reflect-subtypingᴱ H (M $ N) (app₂ v s) p = Left (none-tgt-≮: (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (tgt-none-≮: p)))
+reflect-subtypingᴱ H (M $ N) (beta (function f ⟨ var y ∈ T ⟩∈ U is B end) v refl q) p = Left (≡-trans-≮: (cong tgt (cong orAny (cong typeOfᴹᴼ q))) p)
+reflect-subtypingᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) p = Left p
+reflect-subtypingᴱ H (block var b ∈ T is B end) (block s) p = Left p
+reflect-subtypingᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) p = mapR BlockMismatch (swapLR (≮:-trans p))
+reflect-subtypingᴱ H (block var b ∈ T is done end) done p = mapR BlockMismatch (swapLR (≮:-trans p))
+reflect-subtypingᴱ H (binexp M op N) (binOp₀ s) p = Left (≡-trans-≮: (binOpPreservation H s) p)
+reflect-subtypingᴱ H (binexp M op N) (binOp₁ s) p = Left p
+reflect-subtypingᴱ H (binexp M op N) (binOp₂ s) p = Left p
 
-preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) with heap-weakeningᴮ H B (rednᴱ⊑ s)
-preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | ok p = ok p
-preservationᴮ H (local var x ∈ T ← M ∙ B) (local s) | warning W = warning (block (local₂ W))
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) with remember (typeOfⱽ H v)
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) with T ≡ᵀ U
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just T , p) | yes refl = ok (substitutivityᴮ H B v x (sym p))
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (just U , p) | no q = warning (block (LocalVarMismatch (λ r → q (trans r (cong orNone p)))))
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) with typeOf-val-not-none v
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | ok q = CONTRADICTION (q (sym (cong orNone p)))
-preservationᴮ H (local var x ∈ T ← M ∙ B) (subst v) | (nothing , p) | warning W = warning (block (local₁ W))
-preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) with heap-weakeningᴮ H B (snoc defn)
-preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | ok r = ok (trans r (substitutivityᴮ _ B (addr a) f refl))
-preservationᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) | warning W = warning (block (function₂ W))
-preservationᴮ H (return M ∙ B) (return s) with preservationᴱ H M s
-preservationᴮ H (return M ∙ B) (return s) | ok p = ok p
-preservationᴮ H (return M ∙ B) (return s) | warning (expr W) = warning (block (return W))
-preservationᴮ H (return M ∙ B) (return s) | warning (heap W) = warning (heap W)
+reflect-subtypingᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) p = mapLR (heap-weakeningᴮ _ _ B (snoc defn)) (CONTRADICTION ∘ ≮:-refl) (substitutivityᴮ _ B (addr a) f p)
+reflect-subtypingᴮ H (local var x ∈ T ← M ∙ B) (local s) p = Left (heap-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s) p)
+reflect-subtypingᴮ H (local var x ∈ T ← M ∙ B) (subst v) p = mapR LocalVarMismatch (substitutivityᴮ H B v x p) 
+reflect-subtypingᴮ H (return M ∙ B) (return s) p = mapR return (reflect-subtypingᴱ H M s p)
 
-reflect-substitutionᴱ : ∀ {Γ T} H M v x → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M)
-reflect-substitutionᴱ-whenever-yes : ∀ {Γ T} H v x y (p : x ≡ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever yes p)) → Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))
-reflect-substitutionᴱ-whenever-no : ∀ {Γ T} H v x y (p : x ≢ y) → (just T ≡ typeOfⱽ H v) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever no p)) → Warningᴱ H (typeCheckᴱ H  (Γ ⊕ x ↦ T) (var y))
-reflect-substitutionᴮ : ∀ {Γ T} H B v x → (just T ≡ typeOfⱽ H v) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B)
-reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Warningᴮ H (typeCheckᴮ H Γ′ B)
-reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (just T ≡ typeOfⱽ H v) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Warningᴮ H (typeCheckᴮ H Γ′ B)
+reflect-substitutionᴱ : ∀ {Γ T} H M v x → Warningᴱ H (typeCheckᴱ H Γ (M [ v / x ]ᴱ)) → Either (Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) M)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
+reflect-substitutionᴱ-whenever : ∀ {Γ T} H v x y (p : Dec(x ≡ y)) → Warningᴱ H (typeCheckᴱ H Γ (var y [ v / x ]ᴱwhenever p)) → Either (Warningᴱ H (typeCheckᴱ H (Γ ⊕ x ↦ T) (var y))) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
+reflect-substitutionᴮ : ∀ {Γ T} H B v x → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮ)) → Either (Warningᴮ H (typeCheckᴮ H (Γ ⊕ x ↦ T) B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
+reflect-substitutionᴮ-unless : ∀ {Γ T U} H B v x y (r : Dec(x ≡ y)) → Warningᴮ H (typeCheckᴮ H (Γ ⊕ y ↦ U) (B [ v / x ]ᴮunless r)) → Either (Warningᴮ H (typeCheckᴮ H ((Γ ⊕ x ↦ T) ⊕ y ↦ U) B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
+reflect-substitutionᴮ-unless-yes : ∀ {Γ Γ′ T} H B v x y (r : x ≡ y) → (Γ′ ≡ Γ) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless yes r)) → Either (Warningᴮ H (typeCheckᴮ H Γ′ B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
+reflect-substitutionᴮ-unless-no : ∀ {Γ Γ′ T} H B v x y (r : x ≢ y) → (Γ′ ≡ Γ ⊕ x ↦ T) → Warningᴮ H (typeCheckᴮ H Γ (B [ v / x ]ᴮunless no r)) → Either (Warningᴮ H (typeCheckᴮ H Γ′ B)) (Either (Warningᴱ H (typeCheckᴱ H ∅ (val v))) (typeOfᴱ H ∅ (val v) ≮: T))
 
-reflect-substitutionᴱ H (var y) v x p W with x ≡ⱽ y
-reflect-substitutionᴱ H (var y) v x p W | yes r = reflect-substitutionᴱ-whenever-yes H v x y r p W
-reflect-substitutionᴱ H (var y) v x p W | no r = reflect-substitutionᴱ-whenever-no H v x y r p W
-reflect-substitutionᴱ H (val (addr a)) v x p (UnallocatedAddress r) = UnallocatedAddress r
-reflect-substitutionᴱ H (M $ N) v x p (FunctionCallMismatch q) = FunctionCallMismatch (λ s → q (trans (cong src (sym (substitutivityᴱ H M v x p))) (trans s (substitutivityᴱ H N v x p))))
-reflect-substitutionᴱ H (M $ N) v x p (app₁ W) = app₁ (reflect-substitutionᴱ H M v x p W)
-reflect-substitutionᴱ H (M $ N) v x p (app₂ W) = app₂ (reflect-substitutionᴱ H N v x p W)
-reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
-reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H B v x y r p (⊕-over r))))
-reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H B v x y r p (⊕-swap r))))
-reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) with (x ≡ⱽ y)
-reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
-reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
-reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (BlockMismatch q) = BlockMismatch (λ r → q (trans r (substitutivityᴮ H B v x p)))
-reflect-substitutionᴱ H (block var b ∈ T is B end) v x p (block₁ W) = block₁ (reflect-substitutionᴮ H B v x p W)
-reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₁ q) = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H M x v p)) q)
-reflect-substitutionᴱ H (binexp M op N) x v p (BinOpMismatch₂ q) = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym (substitutivityᴱ H N x v p)) q)
-reflect-substitutionᴱ H (binexp M op N) x v p (bin₁ W) = bin₁ (reflect-substitutionᴱ H M x v p W)
-reflect-substitutionᴱ H (binexp M op N) x v p (bin₂ W) = bin₂ (reflect-substitutionᴱ H N x v p W)
+reflect-substitutionᴱ H (var y) v x W = reflect-substitutionᴱ-whenever H v x y (x ≡ⱽ y) W
+reflect-substitutionᴱ H (val (addr a)) v x (UnallocatedAddress r) = Left (UnallocatedAddress r)
+reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) with substitutivityᴱ H N v x p
+reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Right W = Right (Right W)
+reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q with substitutivityᴱ H M v x (src-any-≮: q)
+reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Left r = Left ((FunctionCallMismatch ∘ any-src-≮: q) r)
+reflect-substitutionᴱ H (M $ N) v x (FunctionCallMismatch p) | Left q | Right W = Right (Right W)
+reflect-substitutionᴱ H (M $ N) v x (app₁ W) = mapL app₁ (reflect-substitutionᴱ H M v x W)
+reflect-substitutionᴱ H (M $ N) v x (app₂ W) = mapL app₂ (reflect-substitutionᴱ H N v x W)
+reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (substitutivityᴮ-unless H B v x y (x ≡ⱽ y) q)
+reflect-substitutionᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) v x (function₁ W) = mapL function₁ (reflect-substitutionᴮ-unless H B v x y (x ≡ⱽ y) W)
+reflect-substitutionᴱ H (block var b ∈ T is B end) v x (BlockMismatch q) =  mapLR BlockMismatch Right (substitutivityᴮ H B v x q)
+reflect-substitutionᴱ H (block var b ∈ T is B end) v x (block₁ W′) = mapL block₁ (reflect-substitutionᴮ H B v x W′)
+reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₁ q) = mapLR BinOpMismatch₁ Right (substitutivityᴱ H M v x q)
+reflect-substitutionᴱ H (binexp M op N) v x (BinOpMismatch₂ q) = mapLR BinOpMismatch₂ Right (substitutivityᴱ H N v x q)
+reflect-substitutionᴱ H (binexp M op N) v x (bin₁ W) = mapL bin₁ (reflect-substitutionᴱ H M v x W)
+reflect-substitutionᴱ H (binexp M op N) v x (bin₂ W) = mapL bin₂ (reflect-substitutionᴱ H N v x W)
 
-reflect-substitutionᴱ-whenever-no H v x y p q (UnboundVariable r) = UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) r)
-reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) with trans p (cong typeOfᴹᴼ q)
-reflect-substitutionᴱ-whenever-yes H (addr a) x x refl p (UnallocatedAddress q) | ()
+reflect-substitutionᴱ-whenever H a x x (yes refl) (UnallocatedAddress p) = Right (Left (UnallocatedAddress p))
+reflect-substitutionᴱ-whenever H v x y (no p) (UnboundVariable q) = Left (UnboundVariable (trans (sym (⊕-lookup-miss x y _ _ p)) q))
 
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) with (x ≡ⱽ y)
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | yes r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-yes H C v x y r p (⊕-over r))))
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (FunctionDefnMismatch q) | no r = FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ-unless-no H C v x y r p (⊕-swap r))))
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) with (x ≡ⱽ y)
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | yes r = function₁ (reflect-substitutionᴮ-unless-yes H C v x y r p (⊕-over r) W)
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₁ W) | no r = function₁ (reflect-substitutionᴮ-unless-no H C v x y r p (⊕-swap r) W)
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W) with (x ≡ⱽ f)
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| yes r = function₂ (reflect-substitutionᴮ-unless-yes H B v x f r p (⊕-over r) W)
-reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x p (function₂ W)| no r = function₂ (reflect-substitutionᴮ-unless-no H B v x f r p (⊕-swap r) W)
-reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (LocalVarMismatch q) = LocalVarMismatch (λ r → q (trans r (substitutivityᴱ H M v x p)))
-reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₁ W) = local₁ (reflect-substitutionᴱ H M v x p W)
-reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) with (x ≡ⱽ y)
-reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | yes r = local₂ (reflect-substitutionᴮ-unless-yes H B v x y r p (⊕-over r) W)
-reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x p (local₂ W) | no r = local₂ (reflect-substitutionᴮ-unless-no H B v x y r p (⊕-swap r) W)
-reflect-substitutionᴮ H (return M ∙ B) v x p (return W) = return (reflect-substitutionᴱ H M v x p W)
+reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (FunctionDefnMismatch q) = mapLR FunctionDefnMismatch Right (substitutivityᴮ-unless H C v x y (x ≡ⱽ y) q)
+reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (function₁ W) =  mapL function₁ (reflect-substitutionᴮ-unless H C v x y (x ≡ⱽ y) W)
+reflect-substitutionᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) v x (function₂ W) = mapL function₂ (reflect-substitutionᴮ-unless H B v x f (x ≡ⱽ f) W)
+reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (LocalVarMismatch q) = mapLR LocalVarMismatch Right (substitutivityᴱ H M v x q)
+reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (local₁ W) = mapL local₁ (reflect-substitutionᴱ H M v x W)
+reflect-substitutionᴮ H (local var y ∈ T ← M ∙ B) v x (local₂ W) = mapL local₂ (reflect-substitutionᴮ-unless H B v x y (x ≡ⱽ y) W)
+reflect-substitutionᴮ H (return M ∙ B) v x (return W) = mapL return (reflect-substitutionᴱ H M v x W)
 
-reflect-substitutionᴮ-unless-yes H B v x y r p refl W = W
-reflect-substitutionᴮ-unless-no H B v x y r p refl W = reflect-substitutionᴮ H B v x p W
+reflect-substitutionᴮ-unless H B v x y (yes p) W = reflect-substitutionᴮ-unless-yes H B v x y p (⊕-over p) W
+reflect-substitutionᴮ-unless H B v x y (no p) W = reflect-substitutionᴮ-unless-no H B v x y p (⊕-swap p) W
+reflect-substitutionᴮ-unless-yes H B v x x refl refl W = Left W
+reflect-substitutionᴮ-unless-no H B v x y p refl W = reflect-substitutionᴮ H B v x W
 
-reflect-weakeningᴱ : ∀ H M {H′ Γ} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M)
-reflect-weakeningᴮ : ∀ H B {H′ Γ} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B)
+reflect-weakeningᴱ : ∀ Γ H M {H′} → (H ⊑ H′) → Warningᴱ H′ (typeCheckᴱ H′ Γ M) → Warningᴱ H (typeCheckᴱ H Γ M)
+reflect-weakeningᴮ : ∀ Γ H B {H′} → (H ⊑ H′) → Warningᴮ H′ (typeCheckᴮ H′ Γ B) → Warningᴮ H (typeCheckᴮ H Γ B)
 
-reflect-weakeningᴱ H (var x) h (UnboundVariable p) = (UnboundVariable p)
-reflect-weakeningᴱ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
-reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) with heap-weakeningᴱ H M h | heap-weakeningᴱ H N h
-reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | ok q₁ | ok q₂ = FunctionCallMismatch (λ r → p (trans (cong src (sym q₁)) (trans r q₂)))
-reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | warning W | _ = app₁ W
-reflect-weakeningᴱ H (M $ N) h (FunctionCallMismatch p) | _ | warning W = app₂ W
-reflect-weakeningᴱ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ H M h W)
-reflect-weakeningᴱ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ H N h W)
-reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) with heap-weakeningᴱ H M h
-reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | ok q = BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p)
-reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₁ p) | warning W = bin₁ W
-reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) with heap-weakeningᴱ H N h
-reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | ok q = BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p)
-reflect-weakeningᴱ H (binexp M op N) h (BinOpMismatch₂ p) | warning W = bin₂ W
-reflect-weakeningᴱ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ H M h W′)
-reflect-weakeningᴱ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ H N h W′)
-reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
-reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
-reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) | warning W = function₁ W
-reflect-weakeningᴱ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ H B h W)
-reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) with heap-weakeningᴮ H B h
-reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | ok q = BlockMismatch (λ r → p (trans r q))
-reflect-weakeningᴱ H (block var b ∈ T is B end) h (BlockMismatch p) | warning W = block₁ W
-reflect-weakeningᴱ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ H B h W)
+reflect-weakeningᴱ Γ H (var x) h (UnboundVariable p) = (UnboundVariable p)
+reflect-weakeningᴱ Γ H (val (addr a)) h (UnallocatedAddress p) = UnallocatedAddress (lookup-⊑-nothing a h p)
+reflect-weakeningᴱ Γ H (M $ N) h (FunctionCallMismatch p) = FunctionCallMismatch (heap-weakeningᴱ Γ H N h (any-src-≮: p (heap-weakeningᴱ Γ H M h (src-any-≮: p))))
+reflect-weakeningᴱ Γ H (M $ N) h (app₁ W) = app₁ (reflect-weakeningᴱ Γ H M h W)
+reflect-weakeningᴱ Γ H (M $ N) h (app₂ W) = app₂ (reflect-weakeningᴱ Γ H N h W)
+reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₁ p) = BinOpMismatch₁ (heap-weakeningᴱ Γ H M h p)
+reflect-weakeningᴱ Γ H (binexp M op N) h (BinOpMismatch₂ p) = BinOpMismatch₂ (heap-weakeningᴱ Γ H N h p)
+reflect-weakeningᴱ Γ H (binexp M op N) h (bin₁ W′) = bin₁ (reflect-weakeningᴱ Γ H M h W′)
+reflect-weakeningᴱ Γ H (binexp M op N) h (bin₂ W′) = bin₂ (reflect-weakeningᴱ Γ H N h W′)
+reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (Γ ⊕ y ↦ T) H B h p)
+reflect-weakeningᴱ Γ H (function f ⟨ var y ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ (Γ ⊕ y ↦ T) H B h W)
+reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (BlockMismatch p) = BlockMismatch (heap-weakeningᴮ Γ H B h p)
+reflect-weakeningᴱ Γ H (block var b ∈ T is B end) h (block₁ W) = block₁ (reflect-weakeningᴮ Γ H B h W)
 
-reflect-weakeningᴮ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ H M h W)
-reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) with heap-weakeningᴱ H M h
-reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | ok q = LocalVarMismatch (λ r → p (trans r q))
-reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) | warning W = local₁ W
-reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ H M h W)
-reflect-weakeningᴮ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ H B h W)
-reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) with heap-weakeningᴮ H C h
-reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
-reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) | warning W = function₁ W
-reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ H C h W)
-reflect-weakeningᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ H B h W)
+reflect-weakeningᴮ Γ H (return M ∙ B) h (return W) = return (reflect-weakeningᴱ Γ H M h W)
+reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (LocalVarMismatch p) = LocalVarMismatch (heap-weakeningᴱ Γ H M h p)
+reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (local₁ W) = local₁ (reflect-weakeningᴱ Γ H M h W)
+reflect-weakeningᴮ Γ H (local var y ∈ T ← M ∙ B) h (local₂ W) = local₂ (reflect-weakeningᴮ (Γ ⊕ y ↦ T) H B h W)
+reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (Γ ⊕ x ↦ T) H C h p)
+reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₁ W) = function₁ (reflect-weakeningᴮ (Γ ⊕ x ↦ T) H C h W)
+reflect-weakeningᴮ Γ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) h (function₂ W) = function₂ (reflect-weakeningᴮ (Γ ⊕ f ↦ (T ⇒ U)) H B h W)
 
 reflect-weakeningᴼ : ∀ H O {H′} → (H ⊑ H′) → Warningᴼ H′ (typeCheckᴼ H′ O) → Warningᴼ H (typeCheckᴼ H O)
-reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) with heap-weakeningᴮ H B h
-reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | ok q = FunctionDefnMismatch (λ r → p (trans r q))
-reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (FunctionDefnMismatch p) | warning W = function₁ W
-reflect-weakeningᴼ H (just (function f ⟨ var x ∈ T ⟩∈ U is B end)) h (function₁ W′) = function₁ (reflect-weakeningᴮ H B h W′)
+reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (FunctionDefnMismatch p) = FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H B h p)
+reflect-weakeningᴼ H (just function f ⟨ var x ∈ T ⟩∈ U is B end) h (function₁ W) = function₁ (reflect-weakeningᴮ (x ↦ T) H B h W)
 
-reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M)
-reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)
+reflectᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴱ H′ (typeCheckᴱ H′ ∅ M′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H))
+reflectᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴮ H′ (typeCheckᴮ H′ ∅ B′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))
 
-reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) with preservationᴱ H M s | heap-weakeningᴱ H N (rednᴱ⊑ s)
-reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p (trans (trans (cong src (sym q)) r) q′)))
-reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (expr W) | _ = expr (app₁ W)
-reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | warning (heap W) | _ = heap W
-reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) | _ | warning W  = expr (app₂ W)
-reflectᴱ H (M $ N) (app₁ s) (app₁ W′) with reflectᴱ H M s W′
-reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | heap W = heap W
-reflectᴱ H (M $ N) (app₁ s) (app₁ W′) | expr W = expr (app₁ W)
-reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = expr (app₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
-reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) with heap-weakeningᴱ H (val p) (rednᴱ⊑ s) | preservationᴱ H N s
-reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | ok q | ok q′ = expr (FunctionCallMismatch (λ r → p′ (trans (trans (cong src (sym q)) r) q′)))
-reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | warning W | _ = expr (app₁ W)
-reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (expr W) = expr (app₂ W)
-reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch p′) | _ | warning (heap W) = heap W
-reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = expr (app₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
-reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) with reflectᴱ H N s W′
-reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | heap W = heap W
-reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) | expr W = expr (app₂ W)
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with remember (typeOfⱽ H v)
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) with S ≡ᵀ T
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just T , r) | yes refl = heap (addr a p (FunctionDefnMismatch (λ s → q (trans s (substitutivityᴮ H B v x (sym r))))))
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (just S , r) | no s = expr (FunctionCallMismatch (λ t → s (trans (cong orNone (sym r)) (trans (sym t) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) with typeOf-val-not-none v
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | ok s = CONTRADICTION (s (cong orNone (sym r)))
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | (nothing , r) | warning W = expr (app₂ W)
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with remember (typeOfⱽ H v)
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) with S ≡ᵀ T
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just T , q) | yes refl = heap (addr a p (function₁ (reflect-substitutionᴮ H B v x (sym q) W′)))
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (just S , q) | no r = expr (FunctionCallMismatch (λ s → r (trans (cong orNone (sym q)) (trans (sym s) (cong src (cong orNone (cong typeOfᴹᴼ p)))))))
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) with typeOf-val-not-none v
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | ok r = CONTRADICTION (r (cong orNone (sym q)))
-reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | (nothing , q) | warning W = expr (app₂ W)
-reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) with preservationᴮ H B s
-reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | ok q = expr (BlockMismatch (λ r → p (trans r q)))
-reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (heap W) = heap W
-reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) | warning (block W) = expr (block₁ W)
-reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) with reflectᴮ H B s W′
-reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | heap W = heap W
-reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) | block W = expr (block₁ W)
-reflectᴱ H (block var b ∈ T is B end) (return v) W′ = expr (block₁ (return W′))
+reflectᴱ H (M $ N) (app₁ s) (FunctionCallMismatch p) = cond (Left ∘ FunctionCallMismatch ∘ heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) ∘ any-src-≮: p) (Left ∘ app₁) (reflect-subtypingᴱ H M s (src-any-≮: p))
+reflectᴱ H (M $ N) (app₁ s) (app₁ W′) = mapL app₁ (reflectᴱ H M s W′)
+reflectᴱ H (M $ N) (app₁ s) (app₂ W′) = Left (app₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′))
+reflectᴱ H (M $ N) (app₂ p s) (FunctionCallMismatch q) = cond (λ r → Left (FunctionCallMismatch (any-src-≮: r (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) (src-any-≮: r))))) (Left ∘ app₂) (reflect-subtypingᴱ H N s q)
+reflectᴱ H (M $ N) (app₂ p s) (app₁ W′) = Left (app₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′))
+reflectᴱ H (M $ N) (app₂ p s) (app₂ W′) = mapL app₂ (reflectᴱ H N s W′)
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) with substitutivityᴮ H B v x q 
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Left r = Right (addr a p (FunctionDefnMismatch r))
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (BlockMismatch q) | Right r = Left (FunctionCallMismatch (≮:-trans-≡ r ((cong src (cong orAny (cong typeOfᴹᴼ (sym p)))))))
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) with reflect-substitutionᴮ _ B v x W′
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Left W = Right (addr a p (function₁ W))
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Left W) = Left (app₂ W)
+reflectᴱ H (val (addr a) $ N) (beta (function f ⟨ var x ∈ T ⟩∈ U is B end) v refl p) (block₁ W′) | Right (Right q) = Left (FunctionCallMismatch (≮:-trans-≡ q (cong src (cong orAny (cong typeOfᴹᴼ (sym p))))))
+reflectᴱ H (block var b ∈ T is B end) (block s) (BlockMismatch p) = Left (cond BlockMismatch block₁ (reflect-subtypingᴮ H B s p))
+reflectᴱ H (block var b ∈ T is B end) (block s) (block₁ W′) = mapL block₁ (reflectᴮ H B s W′)
+reflectᴱ H (block var b ∈ T is B end) (return v) W′ = Left (block₁ (return W′))
 reflectᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (UnallocatedAddress ())
 reflectᴱ H (binexp M op N) (binOp₀ ()) (UnallocatedAddress p)
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) with preservationᴱ H M s
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (heap W) = heap W
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) | warning (expr W) = expr (bin₁ W)
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) with heap-weakeningᴱ H N (rednᴱ⊑ s)
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ ((subst₁ (BinOpWarning op) (sym q) p)))
-reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) | warning W = expr (bin₂ W)
-reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) with reflectᴱ H M s W′
-reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | heap W = heap W
-reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) | expr W = expr (bin₁ W)
-reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = expr (bin₂ (reflect-weakeningᴱ H N (rednᴱ⊑ s) W′))
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) with heap-weakeningᴱ H M (rednᴱ⊑ s)
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | ok q = expr (BinOpMismatch₁ (subst₁ (BinOpWarning op) (sym q) p))
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) | warning W = expr (bin₁ W)
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) with preservationᴱ H N s
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | ok q = expr (BinOpMismatch₂ (subst₁ (BinOpWarning op) (sym q) p))
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (heap W) = heap W
-reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) | warning (expr W) = expr (bin₂ W)
-reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = expr (bin₁ (reflect-weakeningᴱ H M (rednᴱ⊑ s) W′))
-reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) with reflectᴱ H N s W′
-reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | heap W = heap W
-reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) | expr W = expr (bin₂ W)
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₁ p) = Left (cond BinOpMismatch₁ bin₁ (reflect-subtypingᴱ H M s p))
+reflectᴱ H (binexp M op N) (binOp₁ s) (BinOpMismatch₂ p) = Left (BinOpMismatch₂ (heap-weakeningᴱ ∅ H N (rednᴱ⊑ s) p))
+reflectᴱ H (binexp M op N) (binOp₁ s) (bin₁ W′) = mapL bin₁ (reflectᴱ H M s W′)
+reflectᴱ H (binexp M op N) (binOp₁ s) (bin₂ W′) = Left (bin₂ (reflect-weakeningᴱ ∅ H N (rednᴱ⊑ s) W′))
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₁ p) = Left (BinOpMismatch₁ (heap-weakeningᴱ ∅ H M (rednᴱ⊑ s) p))
+reflectᴱ H (binexp M op N) (binOp₂ s) (BinOpMismatch₂ p) = Left (cond BinOpMismatch₂ bin₂ (reflect-subtypingᴱ H N s p))
+reflectᴱ H (binexp M op N) (binOp₂ s) (bin₁ W′) = Left (bin₁ (reflect-weakeningᴱ ∅ H M (rednᴱ⊑ s) W′))
+reflectᴱ H (binexp M op N) (binOp₂ s) (bin₂ W′) = mapL bin₂ (reflectᴱ H N s W′)
 
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) with preservationᴱ H M s
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | ok q = block (LocalVarMismatch (λ r → p (trans r q)))
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (expr W) = block (local₁ W)
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) | warning (heap W) = heap W
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) with reflectᴱ H M s W′
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | heap W = heap W
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) | expr W = block (local₁ W)
-reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = block (local₂ (reflect-weakeningᴮ H B (rednᴱ⊑ s) W′))
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ with remember (typeOfⱽ H v)
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) with S ≡ᵀ T
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just T , p) | yes refl = block (local₂ (reflect-substitutionᴮ H B v x (sym p) W′))
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (just S , p) | no q = block (LocalVarMismatch (λ r → q (trans (cong orNone (sym p)) (sym r))))
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) with typeOf-val-not-none v
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | ok r = CONTRADICTION (r (cong orNone (sym p)))
-reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ | (nothing , p) | warning W = block (local₁ W)
-reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ = block (function₂ (reflect-weakeningᴮ H B (snoc defn) (reflect-substitutionᴮ _ B (addr a) f refl W′)))
-reflectᴮ H (return M ∙ B) (return s) (return W′) with reflectᴱ H M s W′
-reflectᴮ H (return M ∙ B) (return s) (return W′) | heap W = heap W
-reflectᴮ H (return M ∙ B) (return s) (return W′) | expr W = block (return W)
+reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (LocalVarMismatch p) = Left (cond LocalVarMismatch local₁ (reflect-subtypingᴱ H M s p))
+reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₁ W′) = mapL local₁ (reflectᴱ H M s W′)
+reflectᴮ H (local var x ∈ T ← M ∙ B) (local s) (local₂ W′) = Left (local₂ (reflect-weakeningᴮ (x ↦ T) H B (rednᴱ⊑ s) W′))
+reflectᴮ H (local var x ∈ T ← M ∙ B) (subst v) W′ = Left (cond local₂ (cond local₁ LocalVarMismatch) (reflect-substitutionᴮ H B v x W′))
+reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ with reflect-substitutionᴮ _ B (addr a) f W′
+reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Left W = Left (function₂ (reflect-weakeningᴮ (f ↦ (T ⇒ U)) H B (snoc defn) W))
+reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Right (Left (UnallocatedAddress ()))
+reflectᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) W′ | Right (Right p) = CONTRADICTION (≮:-refl p)
+reflectᴮ H (return M ∙ B) (return s) (return W′) = mapL return (reflectᴱ H M s W′)
 
-reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴᴱ H′ (typeCheckᴴᴱ H′ ∅ M′) → Warningᴴᴱ H (typeCheckᴴᴱ H ∅ M)
-reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)
+reflectᴴᴱ : ∀ H M {H′ M′} → (H ⊢ M ⟶ᴱ M′ ⊣ H′) → Warningᴴ H′ (typeCheckᴴ H′) → Either (Warningᴱ H (typeCheckᴱ H ∅ M)) (Warningᴴ H (typeCheckᴴ H))
+reflectᴴᴮ : ∀ H B {H′ B′} → (H ⊢ B ⟶ᴮ B′ ⊣ H′) → Warningᴴ H′ (typeCheckᴴ H′) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))
 
-reflectᴴᴱ H M s (expr W′) = reflectᴱ H M s W′
-reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a
-reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H B (snoc defn)
-reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = expr (FunctionDefnMismatch λ q → p (trans q r))
-reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = expr (function₁ W)
-reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = expr (function₁ (reflect-weakeningᴮ H B (snoc defn) W′))
-reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′))
-reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
-reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | heap W = heap W
-reflectᴴᴱ H (M $ N) (app₁ s) (heap W′) | expr W = expr (app₁ W)
-reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) with reflectᴴᴱ H N s (heap W′)
-reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | heap W = heap W
-reflectᴴᴱ H (M $ N) (app₂ p s) (heap W′) | expr W = expr (app₂ W)
-reflectᴴᴱ H (M $ N) (beta O v p q) (heap W′) = heap W′
-reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) with reflectᴴᴮ H B s (heap W′)
-reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | heap W = heap W
-reflectᴴᴱ H (block var b ∈ T is B end) (block s) (heap W′) | block W = expr (block₁ W)
-reflectᴴᴱ H (block var b ∈ T is return N ∙ B end) (return v) (heap W′) = heap W′
-reflectᴴᴱ H (block var b ∈ T is done end) done (heap W′) = heap W′
-reflectᴴᴱ H (binexp M op N) (binOp₀ s) (heap W′) = heap W′
-reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) with reflectᴴᴱ H M s (heap W′)
-reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | heap W = heap W
-reflectᴴᴱ H (binexp M op N) (binOp₁ s) (heap W′) | expr W = expr (bin₁ W)
-reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) with reflectᴴᴱ H N s (heap W′)
-reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | heap W = heap W
-reflectᴴᴱ H (binexp M op N) (binOp₂ s) (heap W′) | expr W = expr (bin₂ W)
+reflectᴴᴱ H (M $ N) (app₁ s) W = mapL app₁ (reflectᴴᴱ H M s W)
+reflectᴴᴱ H (M $ N) (app₂ v s) W = mapL app₂ (reflectᴴᴱ H N s W)
+reflectᴴᴱ H (M $ N) (beta O v refl p) W = Right W
+reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (addr b refl W) with b ≡ᴬ a
+reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H B (snoc defn) p))
+reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a defn) (addr b refl (function₁ W)) | yes refl = Left (function₁ (reflect-weakeningᴮ (x ↦ T) H B (snoc defn) W))
+reflectᴴᴱ H (function f ⟨ var x ∈ T ⟩∈ U is B end) (function a p) (addr b refl W) | no q = Right (addr b (lookup-not-allocated p q) (reflect-weakeningᴼ H _ (snoc p) W))
+reflectᴴᴱ H (block var b ∈ T is B end) (block s) W = mapL block₁ (reflectᴴᴮ H B s W)
+reflectᴴᴱ H (block var b ∈ T is return (val v) ∙ B end) (return v) W = Right W
+reflectᴴᴱ H (block var b ∈ T is done end) done W = Right W
+reflectᴴᴱ H (binexp M op N) (binOp₀ s) W = Right W
+reflectᴴᴱ H (binexp M op N) (binOp₁ s) W = mapL bin₁ (reflectᴴᴱ H M s W)
+reflectᴴᴱ H (binexp M op N) (binOp₂ s) W = mapL bin₂ (reflectᴴᴱ H N s W)
 
-reflectᴴᴮ H B s (block W′) = reflectᴮ H B s W′
-reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) with reflectᴴᴱ H M s (heap W′)
-reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | heap W = heap W
-reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) (heap W′) | expr W = block (local₁ W)
-reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) (heap W′) = heap W′
-reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) with b ≡ᴬ a
-reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl with heap-weakeningᴮ H C (snoc defn)
-reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | ok r = block (FunctionDefnMismatch (λ q → p (trans q r)))
-reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (FunctionDefnMismatch p))) | yes refl | warning W = block (function₁ W)
-reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a defn) (heap (addr a refl (function₁ W′))) | yes refl = block (function₁ (reflect-weakeningᴮ H C (snoc defn) W′))
-reflectᴴᴮ H (function f ⟨ var y ∈ T ⟩∈ U is C end ∙ B) (function a p) (heap (addr b refl W′)) | no r = heap (addr b (lookup-not-allocated p r) (reflect-weakeningᴼ H _ (snoc p) W′))
-reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) with reflectᴴᴱ H M s (heap W′)
-reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | heap W = heap W
-reflectᴴᴮ H (return M ∙ B) (return s) (heap W′) | expr W = block (return W)
+reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a p) (addr b refl W) with b ≡ᴬ a
+reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (FunctionDefnMismatch p)) | yes refl = Left (FunctionDefnMismatch (heap-weakeningᴮ (x ↦ T) H C (snoc defn) p))
+reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a defn) (addr b refl (function₁ W)) | yes refl = Left (function₁ (reflect-weakeningᴮ (x ↦ T) H C (snoc defn) W))
+reflectᴴᴮ H (function f ⟨ var x ∈ T ⟩∈ U is C end ∙ B) (function a p) (addr b refl W) | no q = Right (addr b (lookup-not-allocated p q) (reflect-weakeningᴼ H _ (snoc p) W))
+reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (local s) W = mapL local₁ (reflectᴴᴱ H M s W)
+reflectᴴᴮ H (local var x ∈ T ← M ∙ B) (subst v) W = Right W
+reflectᴴᴮ H (return M ∙ B) (return s) W = mapL return (reflectᴴᴱ H M s W)
 
-reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Warningᴴᴮ H′ (typeCheckᴴᴮ H′ ∅ B′) → Warningᴴᴮ H (typeCheckᴴᴮ H ∅ B)
+reflect* : ∀ H B {H′ B′} → (H ⊢ B ⟶* B′ ⊣ H′) → Either (Warningᴮ H′ (typeCheckᴮ H′ ∅ B′)) (Warningᴴ H′ (typeCheckᴴ H′)) → Either (Warningᴮ H (typeCheckᴮ H ∅ B)) (Warningᴴ H (typeCheckᴴ H))
 reflect* H B refl W = W
-reflect* H B (step s t) W = reflectᴴᴮ H B s (reflect* _ _ t W)
+reflect* H B (step s t) W = cond (reflectᴮ H B s) (reflectᴴᴮ H B s) (reflect* _ _ t W)
 
-runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → BinOpWarning op (orNone (typeOfⱽ H v))
-runtimeBinOpWarning H v (+ p) = + (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (- p) = - (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (* p) = * (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (/ p) = / (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (< p) = < (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (> p) = > (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (<= p) = <= (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (>= p) = >= (λ q → p (mustBeNumber H ∅ v q))
-runtimeBinOpWarning H v (·· p) = ·· (λ q → p (mustBeString H ∅ v q))
+isntNumber : ∀ H v → (valueType v ≢ number) → (typeOfᴱ H ∅ (val v) ≮: number)
+isntNumber H nil p = scalar-≢-impl-≮: nil number (λ ())
+isntNumber H (addr a) p with remember (H [ a ]ᴴ)
+isntNumber H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar number)
+isntNumber H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar number)
+isntNumber H (number x) p = CONTRADICTION (p refl)
+isntNumber H (bool x) p = scalar-≢-impl-≮: boolean number (λ ())
+isntNumber H (string x) p = scalar-≢-impl-≮: string number (λ ())
+
+isntString : ∀ H v → (valueType v ≢ string) → (typeOfᴱ H ∅ (val v) ≮: string)
+isntString H nil p = scalar-≢-impl-≮: nil string (λ ())
+isntString H (addr a) p with remember (H [ a ]ᴴ)
+isntString H (addr a) p | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (function-≮:-scalar string)
+isntString H (addr a) p | (nothing , q) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ q)) (any-≮:-scalar string)
+isntString H (number x) p = scalar-≢-impl-≮: number string (λ ())
+isntString H (bool x) p = scalar-≢-impl-≮: boolean string (λ ())
+isntString H (string x) p = CONTRADICTION (p refl)
+
+isntFunction : ∀ H v {T U} → (valueType v ≢ function) → (typeOfᴱ H ∅ (val v) ≮: (T ⇒ U))
+isntFunction H nil p = scalar-≮:-function nil
+isntFunction H (addr a) p = CONTRADICTION (p refl)
+isntFunction H (number x) p = scalar-≮:-function number
+isntFunction H (bool x) p = scalar-≮:-function boolean
+isntFunction H (string x) p = scalar-≮:-function string
+
+isntEmpty : ∀ H v → (typeOfᴱ H ∅ (val v) ≮: none)
+isntEmpty H nil = scalar-≮:-none nil
+isntEmpty H (addr a) with remember (H [ a ]ᴴ)
+isntEmpty H (addr a) | (just (function f ⟨ var x ∈ T ⟩∈ U is B end) , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) function-≮:-none
+isntEmpty H (addr a) | (nothing , p) = ≡-trans-≮: (cong orAny (cong typeOfᴹᴼ p)) any-≮:-none
+isntEmpty H (number x) = scalar-≮:-none number
+isntEmpty H (bool x) = scalar-≮:-none boolean
+isntEmpty H (string x) = scalar-≮:-none string
+
+runtimeBinOpWarning : ∀ H {op} v → BinOpError op (valueType v) → (typeOfᴱ H ∅ (val v) ≮: srcBinOp op)
+runtimeBinOpWarning H v (+ p) = isntNumber H v p
+runtimeBinOpWarning H v (- p) = isntNumber H v p
+runtimeBinOpWarning H v (* p) = isntNumber H v p
+runtimeBinOpWarning H v (/ p) = isntNumber H v p
+runtimeBinOpWarning H v (< p) = isntNumber H v p
+runtimeBinOpWarning H v (> p) = isntNumber H v p
+runtimeBinOpWarning H v (<= p) = isntNumber H v p
+runtimeBinOpWarning H v (>= p) = isntNumber H v p
+runtimeBinOpWarning H v (·· p) = isntString H v p
 
 runtimeWarningᴱ : ∀ H M → RuntimeErrorᴱ H M → Warningᴱ H (typeCheckᴱ H ∅ M)
 runtimeWarningᴮ : ∀ H B → RuntimeErrorᴮ H B → Warningᴮ H (typeCheckᴮ H ∅ B)
 
 runtimeWarningᴱ H (var x) UnboundVariable = UnboundVariable refl
 runtimeWarningᴱ H (val (addr a)) (SEGV p) = UnallocatedAddress p
-runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) with typeOf-val-not-none w
-runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | ok q = FunctionCallMismatch (λ r → p (mustBeFunction H ∅ v (λ r′ → q (trans r′ r))))
-runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) | warning W = app₂ W
+runtimeWarningᴱ H (M $ N) (FunctionMismatch v w p) = FunctionCallMismatch (any-src-≮: (isntEmpty H w) (isntFunction H v p))
 runtimeWarningᴱ H (M $ N) (app₁ err) = app₁ (runtimeWarningᴱ H M err)
 runtimeWarningᴱ H (M $ N) (app₂ err) = app₂ (runtimeWarningᴱ H N err)
 runtimeWarningᴱ H (block var b ∈ T is B end) (block err) = block₁ (runtimeWarningᴮ H B err)
@@ -469,6 +343,6 @@ runtimeWarningᴮ H (local var x ∈ T ← M ∙ B) (local err) = local₁ (runt
 runtimeWarningᴮ H (return M ∙ B) (return err) = return (runtimeWarningᴱ H M err)
 
 wellTypedProgramsDontGoWrong : ∀ H′ B B′ → (∅ᴴ ⊢ B ⟶* B′ ⊣ H′) → (RuntimeErrorᴮ H′ B′) → Warningᴮ ∅ᴴ (typeCheckᴮ ∅ᴴ ∅ B)
-wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (block (runtimeWarningᴮ H′ B′ err))
-wellTypedProgramsDontGoWrong H′ B B′ t err | heap (addr a refl ())
-wellTypedProgramsDontGoWrong H′ B B′ t err | block W = W
+wellTypedProgramsDontGoWrong H′ B B′ t err with reflect* ∅ᴴ B t (Left (runtimeWarningᴮ H′ B′ err))
+wellTypedProgramsDontGoWrong H′ B B′ t err | Right (addr a refl ())
+wellTypedProgramsDontGoWrong H′ B B′ t err | Left W = W

prototyping/Properties/Subtyping.agda

@@ -0,0 +1,221 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.Subtyping where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; any; none; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
+open import Luau.Type using (Type; Scalar; strict; nil; number; string; boolean; none; any; _⇒_; _∪_; _∩_; tgt)
+open import Properties.Contradiction using (CONTRADICTION; ¬)
+open import Properties.Equality using (_≢_)
+open import Properties.Functions using (_∘_)
+
+src = Luau.Type.src strict
+
+-- Language membership is decidable
+dec-language : ∀ T t → Either (¬Language T t) (Language T t)
+dec-language nil (scalar number) = Left (scalar-scalar number nil (λ ()))
+dec-language nil (scalar boolean) = Left (scalar-scalar boolean nil (λ ()))
+dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
+dec-language nil (scalar nil) = Right (scalar nil)
+dec-language nil function = Left (scalar-function nil)
+dec-language nil (function-ok t) = Left (scalar-function-ok nil)
+dec-language nil (function-err t) = Right (scalar-function-err nil)
+dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
+dec-language boolean (scalar boolean) = Right (scalar boolean)
+dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
+dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
+dec-language boolean function = Left (scalar-function boolean)
+dec-language boolean (function-ok t) = Left (scalar-function-ok boolean)
+dec-language boolean (function-err t) = Right (scalar-function-err boolean)
+dec-language number (scalar number) = Right (scalar number)
+dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
+dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
+dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
+dec-language number function = Left (scalar-function number)
+dec-language number (function-ok t) = Left (scalar-function-ok number)
+dec-language number (function-err t) = Right (scalar-function-err number)
+dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
+dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
+dec-language string (scalar string) = Right (scalar string)
+dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
+dec-language string function = Left (scalar-function string)
+dec-language string (function-ok t) = Left (scalar-function-ok string)
+dec-language string (function-err t) = Right (scalar-function-err string)
+dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
+dec-language (T₁ ⇒ T₂) function = Right function
+dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t)
+dec-language (T₁ ⇒ T₂) (function-err t) = mapLR function-err function-err (swapLR (dec-language T₁ t))
+dec-language none t = Left none
+dec-language any t = Right any
+dec-language (T₁ ∪ T₂) t = cond (λ p → cond (Left ∘ _,_ p) (Right ∘ right) (dec-language T₂ t)) (Right ∘ left) (dec-language T₁ t)
+dec-language (T₁ ∩ T₂) t = cond (Left ∘ left) (λ p → cond (Left ∘ right) (Right ∘ _,_ p) (dec-language T₂ t)) (dec-language T₁ t)
+
+-- ¬Language T is the complement of Language T
+language-comp : ∀ {T} t → ¬Language T t → ¬(Language T t)
+language-comp t (p₁ , p₂) (left q) = language-comp t p₁ q
+language-comp t (p₁ , p₂) (right q) = language-comp t p₂ q
+language-comp t (left p) (q₁ , q₂) = language-comp t p q₁
+language-comp t (right p) (q₁ , q₂) = language-comp t p q₂
+language-comp (scalar s) (scalar-scalar s p₁ p₂) (scalar s) = p₂ refl
+language-comp (scalar s) (function-scalar s) (scalar s) = language-comp function (scalar-function s) function
+language-comp (scalar s) none (scalar ())
+language-comp function (scalar-function ()) function
+language-comp (function-ok t) (scalar-function-ok ()) (function-ok q)
+language-comp (function-ok t) (function-ok p) (function-ok q) = language-comp t p q
+language-comp (function-err t) (function-err p) (function-err q) = language-comp t q p
+
+-- ≮: is the complement of <:
+¬≮:-impl-<: : ∀ {T U} → ¬(T ≮: U) → (T <: U)
+¬≮:-impl-<: {T} {U} p t q with dec-language U t
+¬≮:-impl-<: {T} {U} p t q | Left r = CONTRADICTION (p (witness t q r))
+¬≮:-impl-<: {T} {U} p t q | Right r = r
+
+<:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U)
+<:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)
+
+-- reflexivity
+≮:-refl : ∀ {T} → ¬(T ≮: T)
+≮:-refl (witness t p q) = language-comp t q p
+
+<:-refl : ∀ {T} → (T <: T)
+<:-refl = ¬≮:-impl-<: ≮:-refl
+
+-- transititivity
+≮:-trans-≡ : ∀ {S T U} → (S ≮: T) → (T ≡ U) → (S ≮: U)
+≮:-trans-≡ p refl = p
+
+≡-trans-≮: : ∀ {S T U} → (S ≡ T) → (T ≮: U) → (S ≮: U)
+≡-trans-≮: refl p = p
+
+≮:-trans : ∀ {S T U} → (S ≮: U) → Either (S ≮: T) (T ≮: U)
+≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t)
+
+<:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U)
+<:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ∘ ≮:-trans)
+
+-- Properties of scalars
+skalar = number ∪ (string ∪ (nil ∪ boolean))
+
+function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
+function-≮:-scalar s = witness function function (scalar-function s)
+
+scalar-≮:-function : ∀ {S T U} → (Scalar U) → (U ≮: (S ⇒ T))
+scalar-≮:-function s = witness (scalar s) (scalar s) (function-scalar s)
+
+any-≮:-scalar : ∀ {U} → (Scalar U) → (any ≮: U)
+any-≮:-scalar s = witness (function-ok (scalar s)) any (scalar-function-ok s)
+
+scalar-≮:-none : ∀ {U} → (Scalar U) → (U ≮: none)
+scalar-≮:-none s = witness (scalar s) (scalar s) none
+
+scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U)
+scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)
+
+-- Properties of tgt
+tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t)
+tgt-function-ok {T = nil} (scalar ())
+tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p
+tgt-function-ok {T = none} (scalar ())
+tgt-function-ok {T = any} p = any
+tgt-function-ok {T = boolean} (scalar ())
+tgt-function-ok {T = number} (scalar ())
+tgt-function-ok {T = string} (scalar ())
+tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p)
+tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p)
+tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)
+
+function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t)
+function-ok-tgt (function-ok p) = p
+function-ok-tgt (left p) = left (function-ok-tgt p)
+function-ok-tgt (right p) = right (function-ok-tgt p)
+function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
+function-ok-tgt any = any
+
+skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
+skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))
+
+skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
+skalar-scalar number = left (scalar number)
+skalar-scalar boolean = right (right (right (scalar boolean)))
+skalar-scalar string = right (left (scalar string))
+skalar-scalar nil = right (right (left (scalar nil)))
+
+tgt-none-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (none ⇒ U)))
+tgt-none-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)
+
+none-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (none ⇒ U))) → (tgt T ≮: U)
+none-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
+none-tgt-≮: (witness function p (q₁ , scalar-function ()))
+none-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂
+none-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ())))
+
+-- Properties of src
+function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t)
+function-err-src {T = nil} none = scalar-function-err nil
+function-err-src {T = T₁ ⇒ T₂} p = function-err p
+function-err-src {T = none} (scalar-scalar number () p)
+function-err-src {T = none} (scalar-function-ok ())
+function-err-src {T = any} none = any
+function-err-src {T = boolean} p = scalar-function-err boolean
+function-err-src {T = number} p = scalar-function-err number
+function-err-src {T = string} p = scalar-function-err string
+function-err-src {T = T₁ ∪ T₂} (left p) = left (function-err-src p)
+function-err-src {T = T₁ ∪ T₂} (right p) = right (function-err-src p)
+function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂
+
+¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
+¬function-err-src {T = nil} (scalar ())
+¬function-err-src {T = T₁ ⇒ T₂} p = function-err p
+¬function-err-src {T = none} any = none
+¬function-err-src {T = any} (scalar ())
+¬function-err-src {T = boolean} (scalar ())
+¬function-err-src {T = number} (scalar ())
+¬function-err-src {T = string} (scalar ())
+¬function-err-src {T = T₁ ∪ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂)
+¬function-err-src {T = T₁ ∩ T₂} (left p) = left (¬function-err-src p)
+¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p)
+
+src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
+src-¬function-err {T = nil} p = none
+src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p
+src-¬function-err {T = none} (scalar-function-err ())
+src-¬function-err {T = any} p = none
+src-¬function-err {T = boolean} p = none
+src-¬function-err {T = number} p = none
+src-¬function-err {T = string} p = none
+src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p)
+src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p)
+src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂)
+
+src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
+src-¬scalar number (scalar number) = none
+src-¬scalar boolean (scalar boolean) = none
+src-¬scalar string (scalar string) = none
+src-¬scalar nil (scalar nil) = none
+src-¬scalar s (left p) = left (src-¬scalar s p)
+src-¬scalar s (right p) = right (src-¬scalar s p)
+src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂)
+src-¬scalar s any = none
+
+src-any-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ any))
+src-any-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p)
+
+any-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ any)) → (U ≮: src T)
+any-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
+any-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
+any-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
+any-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
+
+-- Properties of any and none
+any-≮: : ∀ {T U} → (T ≮: U) → (any ≮: U)
+any-≮: (witness t p q) = witness t any q
+
+none-≮: : ∀ {T U} → (T ≮: U) → (T ≮: none)
+none-≮: (witness t p q) = witness t p none
+
+any-≮:-none : (any ≮: none)
+any-≮:-none = witness (scalar nil) any none
+
+function-≮:-none : ∀ {T U} → ((T ⇒ U) ≮: none)
+function-≮:-none = witness function function none

prototyping/Properties/TypeCheck.agda

@@ -8,7 +8,7 @@ open import Agda.Builtin.Equality using (_≡_; refl)
 open import Agda.Builtin.Bool using (Bool; true; false)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import FFI.Data.Either using (Either)
-open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orNone; tgtBinOp)
+open import Luau.TypeCheck(m) using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orAny; tgtBinOp)
 open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
 open import Luau.Type using (Type; nil; any; none; number; boolean; string; _⇒_; tgt)
 open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
@@ -42,8 +42,8 @@ typeOfⱽ H (string x) = just string
 typeOfᴱ : Heap yes → VarCtxt → (Expr yes) → Type
 typeOfᴮ : Heap yes → VarCtxt → (Block yes) → Type
 
-typeOfᴱ H Γ (var x) = orNone(Γ [ x ]ⱽ)
-typeOfᴱ H Γ (val v) = orNone(typeOfⱽ H v)
+typeOfᴱ H Γ (var x) = orAny(Γ [ x ]ⱽ)
+typeOfᴱ H Γ (val v) = orAny(typeOfⱽ H v)
 typeOfᴱ H Γ (M $ N) = tgt(typeOfᴱ H Γ M)
 typeOfᴱ H Γ (function f ⟨ var x ∈ S ⟩∈ T is B end) = S ⇒ T
 typeOfᴱ H Γ (block var b ∈ T is B end) = T
@@ -64,17 +64,17 @@ mustBeFunction H Γ (string x) p = CONTRADICTION (p refl)
 
 mustBeNumber : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ number) → (valueType(v) ≡ number)
 mustBeNumber H Γ (addr a) p with remember (H [ a ]ᴴ)
-mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
+mustBeNumber H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p
 mustBeNumber H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
-mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
+mustBeNumber H Γ (addr a) p | (nothing , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p
 mustBeNumber H Γ (addr a) p | nothing , q | ()
 mustBeNumber H Γ (number n) p = refl
 
 mustBeString : ∀ H Γ v → (typeOfᴱ H Γ (val v) ≡ string) → (valueType(v) ≡ string)
 mustBeString H Γ (addr a) p with remember (H [ a ]ᴴ)
-mustBeString H Γ (addr a) p | (just O , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
+mustBeString H Γ (addr a) p | (just O , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p
 mustBeString H Γ (addr a) p | (just function f ⟨ var x ∈ T ⟩∈ U is B end , q) | ()
-mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orNone (cong typeOfᴹᴼ (sym q))) p
+mustBeString H Γ (addr a) p | (nothing , q) with trans (cong orAny (cong typeOfᴹᴼ (sym q))) p
 mustBeString H Γ (addr a) p | (nothing , q) | ()
 mustBeString H Γ (string x) p = refl
 
@@ -83,7 +83,7 @@ typeCheckᴮ : ∀ H Γ B → (Γ ⊢ᴮ B ∈ (typeOfᴮ H Γ B))
 
 typeCheckᴱ H Γ (var x) = var refl
 typeCheckᴱ H Γ (val nil) = nil
-typeCheckᴱ H Γ (val (addr a)) = addr (orNone (typeOfᴹᴼ (H [ a ]ᴴ)))
+typeCheckᴱ H Γ (val (addr a)) = addr (orAny (typeOfᴹᴼ (H [ a ]ᴴ)))
 typeCheckᴱ H Γ (val (number n)) = number
 typeCheckᴱ H Γ (val (bool b)) = bool
 typeCheckᴱ H Γ (val (string x)) = string
@@ -109,4 +109,4 @@ typeCheckᴴᴱ H Γ M = (typeCheckᴴ H , typeCheckᴱ H Γ M)
 
 typeCheckᴴᴮ : ∀ H Γ M → (Γ ⊢ᴴᴮ H ▷ M ∈ typeOfᴮ H Γ M)
 typeCheckᴴᴮ H Γ M = (typeCheckᴴ H , typeCheckᴮ H Γ M)
- 
+ 

prototyping/Tests/Interpreter/concat_number_and_string/out.txt

@@ -9,3 +9,4 @@ value 37.0 is not a string
 
 TYPE ERROR:
 Local variable y has type string but expression has type number
+  because provided type contains v, where v is a number

rfcs/STATUS.md

@@ -17,11 +17,10 @@ This document tracks unimplemented RFCs.
 
 ## Sealed/unsealed typing changes
 
-[RFC: Sealed table subtyping](https://github.com/Roblox/luau/blob/master/rfcs/sealed-table-subtyping.md) |
 [RFC: Unsealed table literals](https://github.com/Roblox/luau/blob/master/rfcs/unsealed-table-literals.md) |
 [RFC: Only strip optional properties from unsealed tables during subtyping](https://github.com/Roblox/luau/blob/master/rfcs/unsealed-table-subtyping-strips-optional-properties.md)
 
-**Status**: Implemented but depends on new transaction log implementation that is not fully live yet.
+**Status**: Implemented but not fully rolled out yet.
 
 ## Singleton types
 
@@ -29,14 +28,6 @@ This document tracks unimplemented RFCs.
 
 **Status**: Implemented but not fully rolled out yet.
 
-## Nil-forgiving operator
-
-[RFC: nil-forgiving postfix operator !](https://github.com/Roblox/luau/blob/master/rfcs/syntax-nil-forgiving-operator.md)
-
-**Status**: Needs implementation.
-
-**Notes**: Do we need to reevaluate the necessity given `assert` and improved refinements?
-
 ## Safe navigation operator
 
 [RFC: Safe navigation postfix operator (?)](https://github.com/Roblox/luau/blob/master/rfcs/syntax-safe-navigation-operator.md)
@@ -56,9 +47,3 @@ This document tracks unimplemented RFCs.
 [RFC: Generalized iteration](https://github.com/Roblox/luau/blob/master/rfcs/generalized-iteration.md)
 
 **Status**: Needs implementation
-
-## table.clone
-
-[RFC: table.clone](https://github.com/Roblox/luau/blob/master/rfcs/function-table-clone.md)
-
-**Status**: Needs implementation

rfcs/function-table-clone.md

@@ -1,5 +1,7 @@
 # table.clone
 
+**Status**: Implemented
+
 ## Summary
 
 Add `table.clone` function that, given a table, produces a copy of that table with the same keys/values/metatable.

rfcs/sealed-table-subtyping.md

@@ -1,5 +1,9 @@
 # Sealed table subtyping
 
+**Status**: Implemented
+
+## Summary
+
 In Luau, tables have a state, which can, among others, be "sealed". A sealed table is one that we know the full shape of and cannot have new properties added to it. We would like to introduce subtyping for sealed tables, to allow users to express some subtyping relationships that they currently cannot.
 
 ## Motivation

rfcs/syntax-if-expression.md

@@ -20,7 +20,7 @@ Instead of `and/or`, `if/else` statement can be used but since that requires a s
 
 To solve these problems, we propose introducing a first-class ternary conditional. Instead of `? :` common in C-like languages, we propose an `if-then-else` expression form that is syntactically similar to `if-then-else` statement, but lacks terminating `end`.
 
-Concretely, the `if-then-else` expression must match `if <expr> then <expr> else <expr>`; it can also contain an arbitrary number of `elseif` clauses, like `if <expr> then <expr> elseif <expr> then <expr> else <expr>`. Note that in either case, `else` is mandatory.
+Concretely, the `if-then-else` expression must match `if <expr> then <expr> else <expr>`; it can also contain an arbitrary number of `elseif` clauses, like `if <expr> then <expr> elseif <expr> then <expr> else <expr>`. Unlike if statements, `else` is mandatory.
 
 The result of the expression is the then-expression when condition is truthy (not `nil` or `false`) and else-expression otherwise. Only one of the two possible resulting expressions is evaluated.
 
@@ -30,11 +30,27 @@ Example:
 local x = if FFlagFoo then A else B
 
 MyComponent.validateProps = t.strictInterface({
-	layoutOrder = t.optional(t.number),
-	newThing = if FFlagUseNewThing then t.whatever() else nil,
+    layoutOrder = t.optional(t.number),
+    newThing = if FFlagUseNewThing then t.whatever() else nil,
 })
 ```
 
+Note that `else` is mandatory because it's always better to be explicit. If it weren't mandatory, it opens the possiblity that someone might be writing a chain of if-then-else and forgot to add in the final `else` that _doesn't_ return a `nil` value! Enforcing this syntactically ensures the program does not run. Also, with it being mandatory, it solves many cases where parsing the expression is ambiguous due to the infamous [dangling else](https://en.wikipedia.org/wiki/Dangling_else).
+
+This example will not do what it looks like it's supposed to do! The if expression will _successfully_ parse and be interpreted as to return `h()` if `g()` evaluates to some falsy value, when in actual fact the clear intention is to evaluate `h()` only if `f()` is falsy.
+
+```lua
+if f() then
+    ...
+    local foo = if g() then x
+else
+    h()
+    ...
+end
+```
+
+The only way to solve this had we chose optional `else` branch would be to wrap the if expression in parentheses or to place a semi-colon. 
+
 ## Drawbacks
 
 Studio's script editor autocomplete currently adds an indented block followed by `end` whenever a line ends that includes a `then` token. This can make use of the if expression unpleasant as developers have to keep fixing the code by removing auto-inserted `end`. We can work around this on the editor side by (short-term) differentiating between whether `if` token is the first on its line, and (long-term) by refactoring completion engine to use infallible parser for the block completer.

rfcs/syntax-nil-forgiving-operator.md

@@ -1,90 +0,0 @@
-# nil-forgiving postfix operator !
-
-## Summary
-
-Introduce syntax to suppress typechecking errors for nilable types by ascribing them into a non-nil type.
-
-## Motivation
-
-Typechecking might not be able to figure out that a certain expression is a non-nil type, but the user might know additional context of the expression.
-
-Using `::` ascriptions is the current work-around for this issue, but it's much more verbose and requires providing the full type name when you only want to ascribe T? to T.
-
-The nil-forgiving operator will also allow chaining to be written in a very terse manner:
-```lua
-local p = a!.b!.c
-```
-instead of
-```lua
-local ((p :: Part).b :: Folder).c
-```
-
-Note that nil-forgiving operator is **not** a part of member access operator, it can be used in standalone expressions, indexing and other places:
-```lua
-local p = f(a!)!
-local q = b!['X']
-```
-
-Nil-forgiving operator can be found in some programming languages such as C# (null-forgiving or null-suppression operator) and TypeScript (non-null assertion operator).
-
-## Design
-
-To implement this, we will change the syntax of the *primaryexp*.
-
-Before:
-```
-primaryexp ::= prefixexp { `.' NAME | `[' exp `]' | `:' NAME funcargs | funcargs }
-```
-After:
-```
-postfixeexp ::= (`.' NAME | `[' exp `]' | `:' NAME funcargs | funcargs) [`!']
-primaryexp ::= prefixexp [`!'] { postfixeexp }
-```
-
-When we get the `!` token, we will wrap the expression that we have into a new AstExprNonNilAssertion node.
-
-An error is generated when the type of expression node this is one of the following:
-* AstExprConstantBool
-* AstExprConstantNumber
-* AstExprConstantString
-* AstExprFunction
-* AstExprTable
-
-This operator doesn't have any impact on the run-time behavior of the program, it will only affect the type of the expression in the typechecker.
-
----
-While parsing an assignment expression starts with a *primaryexp*, it performs a check that it has an l-value based on a fixed set of AstNode types.
-
-Since using `!` on an l-value has no effect, we don't extend this list with the new node and will generate a specialized parse error for code like:
-```lua
-p.a! = b
-```
-
----
-When operator is used on expression of a union type with a `nil` option, it removes that option from the set.
-If only one option remains, the union type is replaced with the type of a single option.
-
-If the type is `nil`, typechecker will generate a warning that the operator cannot be applied to the expression.
-
-For any other type, it has no effect and doesn't generate additional warnings.
-
-The reason for the last rule is to simplify movement of existing code where context in each location is slightly different.
-
-As an example from Roblox, instance path could dynamically change from being know to exist to be missing when script is changed in edit mode.
-
-## Drawbacks
-
-### Unnecessary operator use
-
-It might be useful to warn about unnecessary uses of this operator when the value cannot be `nil`, but we have no way of enabling this behavior.
-
-### Bad practice
-
-The operator might be placed by users to ignore/silence correct warnings and lower the strength of type checking that Luau provides.
-
-## Alternatives
-
-Aside from type assertion operator :: it should be possible to place `assert` function calls before the operation.
-Type refinement/constraints should handle that statement and avoid warning in the following expressions.
-
-But `assert` call will introduce runtime overhead without adding extra safety to the case when the type is nil at run time, in both cases an error will be thrown.