Tidy up semantic subtyping

.github/workflows/test.yml

@@ -10,9 +10,9 @@ jobs:
   linux:
     strategy:
       matrix:
-        agda: [2.6.2.2]
-        hackageDate: ["2022-12-08"]
-        hackageTime: ["00:41:16"]
+        agda: [2.6.4]
+        hackageDate: ["2023-12-01"]
+        hackageTime: ["20:29:20"]
     runs-on: ubuntu-latest
     steps:
     - uses: actions/checkout@v1
@@ -26,15 +26,15 @@ jobs:
       run: cabal v2-update "hackage.haskell.org,${{ matrix.hackageDate }}T${{ matrix.hackageTime }}Z"
     - name: cabal install
       run: |
-        cabal install --lib scientific vector aeson --package-env .
+        cabal install --lib text bytestring scientific vector aeson --package-env .
         cabal install --allow-newer Agda-${{ matrix.agda }}
     - name: check targets
       run: |
-        ~/.cabal/bin/agda Everything.agda
+        ~/.local/bin/agda Everything.agda
     - name: build executables
       run: |
-        ~/.cabal/bin/agda --compile PrettyPrinter.agda
-        ~/.cabal/bin/agda --compile Interpreter.agda
+        ~/.local/bin/agda --compile PrettyPrinter.agda
+        ~/.local/bin/agda --compile Interpreter.agda
     - name: clone Luau
       uses: actions/checkout@v2
       with:

Luau/ErrorSuppression.agda

@@ -5,7 +5,7 @@ module Luau.ErrorSuppression where
 open import Agda.Builtin.Unit using (⊤)
 open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond)
 open import Luau.Type using (Type; unknown; never; any; error; funktion; scalar; _⇒_; _∪_; _∩_)
-open import Luau.Subtyping using (Value; TypedValue; Arguments; Result; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; warning; witness; ⟨untyped⟩; error; diverge; scalar; ⟨⟩)
+open import Luau.Subtyping using (Value; TypedValue; Arguments; Result; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; check; witness; ⟨untyped⟩; error; diverge; scalar; ⟨⟩)
 open import Properties.Contradiction using (¬; ⊥)
 open import Properties.Product using (_×_)
 
@@ -21,7 +21,6 @@ SuppressedValue T ⟨ t ⟩ = SuppressedTypedValue T t
 
 SuppressedTypedValue (scalar S) t = ⊥
 SuppressedTypedValue (S ⇒ T) (scalar s) = ⊥
-SuppressedTypedValue (S ⇒ T) (warning s) = SuppressedValue S s
 SuppressedTypedValue (S ⇒ T) (s ↦ t) = Either (SuppressedArguments S s) (SuppressedResult T t)
 SuppressedTypedValue never t = ⊥
 SuppressedTypedValue any t = ⊤
@@ -35,6 +34,7 @@ SuppressedArguments T ⟨ t ⟩ = SuppressedTypedValue T t
 
 SuppressedResult T error = Language T error
 SuppressedResult T diverge = ⊥
+SuppressedResult T check = ⊥
 SuppressedResult T ⟨ t ⟩ = SuppressedTypedValue T t
 
 -- A subtyping failure which should not be suppressed

Luau/StrictMode/ToString.agda

@@ -4,7 +4,7 @@ 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 (_≮:_; TypedValue; error; witness; scalar; warning; diverge; ⟨untyped⟩; function-ok; function-warning; _↦_; ⟨⟩; ⟨_⟩)
+open import Luau.Subtyping using (_≮:_; TypedValue; error; witness; scalar; check; diverge; ⟨untyped⟩; function-ok; _↦_; ⟨⟩; ⟨_⟩)
 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; NotFunctionCall; UnsafeFunction; UnsafeBlock; UnsafeLocal)
 open import Luau.Syntax using (Expr; val; yes; var; var_∈_; _⟨_⟩∈_; _$_; addr; num; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name)
 open import Luau.Type using (NUMBER; BOOLEAN; STRING; NIL; _⇒_)
@@ -29,13 +29,14 @@ valueToString (scalar STRING) n v = v ++ " is a string"
 valueToString (scalar NIL) n v = v ++ " is nil"
 valueToString (⟨ s ⟩ ↦ ⟨ t ⟩) n v = valueToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n  " ++ valueToString s (suc n) w where w = tmp n
 valueToString (⟨⟩ ↦ ⟨ t ⟩) n v = valueToString t n (v ++ "()")
-valueToString (warning ⟨ t ⟩) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ valueToString t (suc n) w where w = tmp n
-valueToString (warning error) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ w ++ " is untyped" where w = tmp n
+valueToString (⟨⟩ ↦ check) n v = v ++ "() can check that an argument is provided"
 valueToString (⟨⟩ ↦ error) n v = v ++ "() can error"
 valueToString (⟨⟩ ↦ diverge) n v = v ++ "() can diverge"
+valueToString (⟨untyped⟩ ↦ check) n v = v ++ "(" ++ w ++ ") can fail a check when\n  " ++ w ++ " is untyped" where w = tmp n
 valueToString (⟨untyped⟩ ↦ error) n v = v ++ "(" ++ w ++ ") can error when\n  " ++ w ++ " is untyped" where w = tmp n
 valueToString (⟨untyped⟩ ↦ diverge) n v = v ++ "(" ++ w ++ ") can diverge when\n  " ++ w ++ " is untyped" where w = tmp n
 valueToString (⟨untyped⟩ ↦ ⟨ t ⟩) n v = valueToString t (suc n) (v ++ "(" ++ w ++ ")") ++ " when\n  " ++ w ++ " is untyped" where w = tmp n
+valueToString (⟨ s ⟩ ↦ check) n v = v ++ "(" ++ w ++ ")" ++ "can fail a check when\n  " ++ valueToString s (suc n) w where w = tmp n
 valueToString (⟨ s ⟩ ↦ error) n v = v ++ "(" ++ w ++ ")" ++ "can error when\n  " ++ valueToString s (suc n) w where w = tmp n
 valueToString (⟨ s ⟩ ↦ diverge) n v = v ++ "(" ++ w ++ ")" ++ "can diverge when\n  " ++ valueToString s (suc n) w where w = tmp n
 

Luau/Subtyping.agda

@@ -17,7 +17,6 @@ data Value : Set
 data TypedValue where
 
   scalar : Scalar → TypedValue
-  warning : Value → TypedValue
   _↦_ : Arguments → Result → TypedValue
 
 data Arguments where
@@ -29,9 +28,10 @@ data Arguments where
 
 data Result where
 
-  -- The effects we're tracking are causing a runtime error, a typecheck warning,
+  -- The effects we're tracking are causing a runtime error, an argument check failing,
   -- or diverging
   error : Result
+  check : Result
   diverge : Result
   ⟨_⟩ : TypedValue → Result
 
@@ -46,13 +46,14 @@ data RLanguage : Type → Result → Set
 data ¬RLanguage : Type → Result → Set
 data ALanguage : Type → Arguments → Set
 data ¬ALanguage : Type → Arguments → Set
+data ¬NoneCheck : Arguments → Result → Set
 
 data Language where
 
   scalar : ∀ T → Language (scalar T) ⟨ scalar T ⟩
   function-nok : ∀ {T U t u} → (¬ALanguage T t) → Language (T ⇒ U) ⟨ t ↦ u ⟩
   function-ok : ∀ {T U t u} → (RLanguage U u) → Language (T ⇒ U) ⟨ t ↦ u ⟩
-  function-warning : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) ⟨ warning t ⟩
+  function-none-check : ∀ {T U} → Language (T ⇒ U) ⟨ ⟨⟩ ↦ check ⟩
   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
@@ -63,11 +64,9 @@ data ¬Language where
 
   scalar-scalar : ∀ S T → (S ≢ T) → ¬Language (scalar T) ⟨ scalar S ⟩
   scalar-function : ∀ S {t u} → ¬Language (scalar S) ⟨ t ↦ u ⟩
-  scalar-warning : ∀ {T t} → ¬Language (scalar T) ⟨ warning t ⟩
   scalar-error : ∀ S → ¬Language (scalar S) error
   function-scalar : ∀ S {T U} → ¬Language (T ⇒ U) ⟨ scalar S ⟩
-  function-function : ∀ {T U t u} → (ALanguage T t) → (¬RLanguage U u) → ¬Language (T ⇒ U) ⟨ t ↦ u ⟩
-  function-warning : ∀ {T U t} → Language T t → ¬Language (T ⇒ U) ⟨ warning t ⟩
+  function-function : ∀ {T U t u} → (ALanguage T t) → (¬RLanguage U u) → (¬NoneCheck t u) → ¬Language (T ⇒ U) ⟨ t ↦ u ⟩
   function-error : ∀ {T U} → ¬Language (T ⇒ U) error
   _,_ : ∀ {T U t} → ¬Language T t → ¬Language U t → ¬Language (T ∪ U) t
   left : ∀ {T U t} → ¬Language T t → ¬Language (T ∩ U) t
@@ -84,6 +83,7 @@ data RLanguage where
 data ¬RLanguage where
 
   error : ∀ {T} → ¬Language T error → ¬RLanguage T error
+  check : ∀ {T} → ¬RLanguage T check
   one : ∀ {T t} → ¬Language T ⟨ t ⟩ → ¬RLanguage T ⟨ t ⟩
 
 data ALanguage where
@@ -97,6 +97,14 @@ data ¬ALanguage where
   untyped : ∀ {T} → ¬Language T error → ¬ALanguage T ⟨untyped⟩
   one : ∀ {T t} → ¬Language T ⟨ t ⟩ → ¬ALanguage T ⟨ t ⟩
 
+data ¬NoneCheck where
+
+  one₁ : ∀ {t u} → ¬NoneCheck ⟨ t ⟩ u
+  one₂ : ∀ {t u} → ¬NoneCheck t ⟨ u ⟩
+  error : ∀ {t} → ¬NoneCheck t error
+  diverge : ∀ {t} → ¬NoneCheck t diverge
+  untyped : ∀ {u} → ¬NoneCheck ⟨untyped⟩ u
+
 -- Subtyping as language inclusion
 
 _<:_ : Type → Type → Set

Properties/DecSubtyping.agda

@@ -4,7 +4,7 @@ module Properties.DecSubtyping 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 (_<:_; _≮:_; Language; ¬Language; witness; any; never; scalar; error; warning; scalar-function; scalar-scalar; function-scalar; function-ok; function-nok; function-error; function-warning; function-function; none; one; untyped; left; right; _,_; _↦_; ⟨⟩; ⟨_⟩; ⟨untyped⟩)
+open import Luau.Subtyping using (_<:_; _≮:_; Language; ¬Language; witness; any; never; scalar; error; scalar-function; scalar-scalar; function-scalar; function-ok; function-nok; function-error; function-function; none; one; one₁; one₂; check; untyped; left; right; _,_; _↦_; ⟨⟩; ⟨_⟩; ⟨untyped⟩)
 open import Luau.Type using (Type; Scalar; scalar; never; any; _⇒_; _∪_; _∩_)
 open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)
 open import Luau.TypeSaturation using (saturate)
@@ -51,7 +51,8 @@ dec-subtypingˢᶠ {F} Fᶠ (defn sat-∩ sat-∪) (S ⇒ T) = result (top Fᶠ
 
   result : Top F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
   result (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-subtyping S Sᵗ
-  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness Ss ¬Sᵗs) = Left (witness (ov-language Fᶠ (λ o → function-warning (<:-impl-⊇ (srcᵗ o) ¬Sᵗs))) (function-warning Ss))
+  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness {error} Se ¬Sᵗe) = Left (witness (ov-language Fᶠ (λ o → function-nok (untyped (<:-impl-⊇ (srcᵗ o) ¬Sᵗe)))) (function-function (untyped Se) check untyped))
+  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness {⟨ s ⟩} Ss ¬Sᵗs) = Left (witness (ov-language Fᶠ (λ o → function-nok (one (<:-impl-⊇ (srcᵗ o) ¬Sᵗs)))) (function-function (one Ss) check one₁))
   result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Right S<:Sᵗ = result₀ (largest Fᶠ (λ o → o)) where
 
     data LargestSrc (G : Type) : Set where
@@ -90,8 +91,8 @@ dec-subtypingˢᶠ {F} Fᶠ (defn sat-∩ sat-∪) (S ⇒ T) = result (top Fᶠ
          })
 
     result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <:ᵒ (S ⇒ T))
-    result₀ (no S₀ T₀ o₀ (witness {error} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ error ⟩} (ov-language Fᶠ (λ o → function-ok (error (tgt₀ o T₀t)))) (function-function none (error ¬Tt)))
-    result₀ (no S₀ T₀ o₀ (witness {⟨ t ⟩} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩} (ov-language Fᶠ (λ o → function-ok (one (tgt₀ o T₀t)))) (function-function none (one ¬Tt)))
+    result₀ (no S₀ T₀ o₀ (witness {error} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ error ⟩} (ov-language Fᶠ (λ o → function-ok (error (tgt₀ o T₀t)))) (function-function none (error ¬Tt) error))
+    result₀ (no S₀ T₀ o₀ (witness {⟨ t ⟩} T₀t ¬Tt) tgt₀) = Left (witness {t = ⟨ ⟨⟩ ↦ ⟨ t ⟩ ⟩} (ov-language Fᶠ (λ o → function-ok (one (tgt₀ o T₀t)))) (function-function none (one ¬Tt) one₂))
     result₀ (yes S₀ T₀ o₀ T₀<:T src₀) with dec-subtyping S S₀
     result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right λ { here → defn o₀ S<:S₀ T₀<:T }
     result₀ (yes S₀ T₀ o₀ T₀<:T src₀) | Left (witness {s} Ss ¬S₀s) = Left (result₁ s Ss ¬S₀s (smallest Fᶠ (λ o → o))) where
@@ -120,28 +121,28 @@ dec-subtypingˢᶠ {F} Fᶠ (defn sat-∩ sat-∪) (S ⇒ T) = result (top Fᶠ
       result₁ : ∀ s → Language S s → ¬Language S₀ s → SmallestTgt F s → (F ≮: (S ⇒ T))
       result₁ s Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) with dec-subtyping T₁ T
       result₁ s Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp ¬S₀s (src₀ o₁ T₁<:T S₁s))
-      result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (error ¬Tt)) where
+      result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (error ¬Tt) error) where
 
         lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨untyped⟩ ↦ error ⟩
         lemma {S′} {T′} o with dec-language S′ error
         lemma {S′} {T′} o | Left ¬S′e = function-nok (untyped ¬S′e)
         lemma {S′} {T′} o | Right S′e = function-ok (error (tgt₁ o S′e T₁t))
 
-      result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (one ¬Tt)) where
+      result₁ error Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (untyped Ss) (one ¬Tt) one₂) where
 
         lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨untyped⟩ ↦ ⟨ t ⟩ ⟩
         lemma {S′} {T′} o with dec-language S′ error
         lemma {S′} {T′} o | Left ¬S′e = function-nok (untyped ¬S′e)
         lemma {S′} {T′} o | Right S′e = function-ok (one (tgt₁ o S′e T₁t))
 
-      result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (error ¬Tt)) where
+      result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {error} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (error ¬Tt) one₁) where
 
         lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨ s ⟩ ↦ error ⟩
         lemma {S′} {T′} o with dec-language S′ ⟨ s ⟩
         lemma {S′} {T′} o | Left ¬S′s = function-nok (one ¬S′s)
         lemma {S′} {T′} o | Right S′s = function-ok (error (tgt₁ o S′s T₁t))
 
-      result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (one ¬Tt)) where
+      result₁ ⟨ s ⟩ Ss ¬S₀s (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness {⟨ t ⟩} T₁t ¬Tt) = witness (ov-language Fᶠ lemma) (function-function (one Ss) (one ¬Tt) one₁) where
 
         lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) ⟨ ⟨ s ⟩ ↦ ⟨ t ⟩ ⟩
         lemma {S′} {T′} o with dec-language S′ ⟨ s ⟩

Properties/ErrorSuppression.agda

@@ -4,7 +4,7 @@ module Properties.ErrorSuppression where
 
 open import FFI.Data.Either using (Either; Left; Right; mapL; mapR; mapLR; swapLR; cond)
 open import Luau.Type using (Type; unknown; never; any; error; funktion; scalar; _⇒_; _∪_; _∩_)
-open import Luau.Subtyping using (Value; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; ⟨⟩; ⟨untyped⟩; warning; witness; scalar; function-nok; function-ok; function-warning; left; right; _,_; any; error; untyped; one; diverge; scalar-scalar; scalar-function; scalar-warning; scalar-error; function-scalar; function-function; function-error; never; none)
+open import Luau.Subtyping using (Value; Language; ¬Language; _<:_; _≮:_; ⟨_⟩; _↦_; ⟨⟩; ⟨untyped⟩; check; witness; scalar; function-nok; function-ok; left; right; _,_; any; error; untyped; one; diverge; scalar-scalar; scalar-function; scalar-error; function-scalar; function-function; function-error; never; none)
 open import Luau.ErrorSuppression using (SuppressedValue; SuppressedTypedValue; SuppressedArguments;  SuppressedResult; _≮:ᵘ_; _,_)
 open import Luau.SafeTypes using (Unsafe; any; error; param; result; ∪-left; ∪-right; ∩-left; ∩-right)
 open import Properties.Contradiction using (¬; ⊥)
@@ -28,8 +28,6 @@ dec-SuppressedValue T ⟨ t ⟩ = dec-SuppressedTypedValue T t
 
 dec-SuppressedTypedValue (scalar s) t = Right (λ ())
 dec-SuppressedTypedValue (S ⇒ T) (scalar s) = Right (λ ())
-dec-SuppressedTypedValue (S ⇒ T) (warning error) = mapL param (dec-SuppressedValue S error)
-dec-SuppressedTypedValue (S ⇒ T) (warning ⟨ s ⟩) = mapL param (dec-SuppressedTypedValue S s)
 dec-SuppressedTypedValue (S ⇒ T) (s ↦ t) with dec-SuppressedArguments S s
 dec-SuppressedTypedValue (S ⇒ T) (s ↦ t) | Left p = Left (param p)
 dec-SuppressedTypedValue (S ⇒ T) (s ↦ t) | Right p = mapLR result (cond p) (dec-SuppressedResult T t)
@@ -50,6 +48,7 @@ dec-SuppressedArguments T ⟨ t ⟩ = dec-SuppressedTypedValue T t
 dec-SuppressedResult T error = dec-SuppressedValue T error
 dec-SuppressedResult T diverge = Right (λ ())
 dec-SuppressedResult T ⟨ t ⟩ = dec-SuppressedTypedValue T t
+dec-SuppressedResult T check = Right (λ ())
 
 dec-Unsafe-≮:ᵘ : ∀ {T U} → (T ≮: U) → Either (Unsafe T) (T ≮:ᵘ U)
 dec-Unsafe-≮:ᵘ {T} (witness {t} p q) = mapR (λ r → (witness p q , r)) (dec-SuppressedValue T t)