From 87edc86c3461ea3e4d09d608df4afdf4d1c23370 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Mar 2025 16:29:29 +0100 Subject: [PATCH 1/4] Fixing the typesetting rule --- dhall/src/Dhall/TypeCheck.hs | 30 +++++++++++++++++++++++++++++- 1 file changed, 29 insertions(+), 1 deletion(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 9c2a30355..2a9fcd8a3 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -1314,12 +1314,40 @@ infer typer = loop VOptional _O' -> do case ks of - WithQuestion :| _ -> do + -- The old rule was: + -- + -- Γ ⊢ e : Optional T + -- Γ ⊢ v : T' + -- T === T' + -- ────────────────────────────────── + -- Γ ⊢ e with ?.ks… = v : Optional T + -- + -- Here T is _O' and T' = tV'. + -- + -- The new rule is: + -- + -- Γ ⊢ e : Optional T + -- Γ, x : T ⊢ x with ks… = v : T₁ + -- T ≡ T₁ + -- ────────────────────────────────── x ∉ FV(v) + -- Γ ⊢ e with ?.ks… = v : Optional T + -- + -- Here T is _O' and T₁ is tV'. + + -- (Some x) with ? = v is valid iff the type of x is the same as the type of v. + WithQuestion :| [] -> do tV' <- loop ctx v if Eval.conv values _O' tV' then return (VOptional _O') else die OptionalWithTypeMismatch + -- (Some x) with ?.a.b = v is valid iff the type of x.a.b is the same as the type of v. + WithQuestion :| k₁ : ks' -> do + tV' <- with _O' (k₁ :| ks') v + if Eval.conv values _O' tV' + then return (VOptional _O') + else die OptionalWithTypeMismatch + WithLabel k :| _ -> die (NotAQuestionPath k) _ -> die (NotWithARecord e₀ (quote names tE')) -- TODO: NotWithARecordOrOptional From 215d4d1b0b23112e851ecccf562b1057958dee85 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Mar 2025 18:50:35 +0100 Subject: [PATCH 2/4] remove extraneous comment and refactor --- dhall/src/Dhall/TypeCheck.hs | 32 +++++--------------------------- 1 file changed, 5 insertions(+), 27 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 2a9fcd8a3..ef520d3a1 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -1314,36 +1314,14 @@ infer typer = loop VOptional _O' -> do case ks of - -- The old rule was: - -- - -- Γ ⊢ e : Optional T - -- Γ ⊢ v : T' - -- T === T' - -- ────────────────────────────────── - -- Γ ⊢ e with ?.ks… = v : Optional T - -- - -- Here T is _O' and T' = tV'. - -- - -- The new rule is: - -- - -- Γ ⊢ e : Optional T - -- Γ, x : T ⊢ x with ks… = v : T₁ - -- T ≡ T₁ - -- ────────────────────────────────── x ∉ FV(v) - -- Γ ⊢ e with ?.ks… = v : Optional T - -- - -- Here T is _O' and T₁ is tV'. -- (Some x) with ? = v is valid iff the type of x is the same as the type of v. - WithQuestion :| [] -> do - tV' <- loop ctx v - if Eval.conv values _O' tV' - then return (VOptional _O') - else die OptionalWithTypeMismatch - -- (Some x) with ?.a.b = v is valid iff the type of x.a.b is the same as the type of v. - WithQuestion :| k₁ : ks' -> do - tV' <- with _O' (k₁ :| ks') v + WithQuestion :| ks' -> do + let typecheckLhs = case ks' of + [] -> loop ctx v + k₁ : ks' -> with _O' (k₁ :| ks') v + tV' <- typecheckLhs if Eval.conv values _O' tV' then return (VOptional _O') else die OptionalWithTypeMismatch From 3ad8f58f943b7011eeb623312010ca689e57f14e Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Mar 2025 19:05:22 +0100 Subject: [PATCH 3/4] Revert "remove extraneous comment and refactor" This reverts commit 215d4d1b0b23112e851ecccf562b1057958dee85. --- dhall/src/Dhall/TypeCheck.hs | 32 +++++++++++++++++++++++++++----- 1 file changed, 27 insertions(+), 5 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index ef520d3a1..2a9fcd8a3 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -1314,14 +1314,36 @@ infer typer = loop VOptional _O' -> do case ks of + -- The old rule was: + -- + -- Γ ⊢ e : Optional T + -- Γ ⊢ v : T' + -- T === T' + -- ────────────────────────────────── + -- Γ ⊢ e with ?.ks… = v : Optional T + -- + -- Here T is _O' and T' = tV'. + -- + -- The new rule is: + -- + -- Γ ⊢ e : Optional T + -- Γ, x : T ⊢ x with ks… = v : T₁ + -- T ≡ T₁ + -- ────────────────────────────────── x ∉ FV(v) + -- Γ ⊢ e with ?.ks… = v : Optional T + -- + -- Here T is _O' and T₁ is tV'. -- (Some x) with ? = v is valid iff the type of x is the same as the type of v. + WithQuestion :| [] -> do + tV' <- loop ctx v + if Eval.conv values _O' tV' + then return (VOptional _O') + else die OptionalWithTypeMismatch + -- (Some x) with ?.a.b = v is valid iff the type of x.a.b is the same as the type of v. - WithQuestion :| ks' -> do - let typecheckLhs = case ks' of - [] -> loop ctx v - k₁ : ks' -> with _O' (k₁ :| ks') v - tV' <- typecheckLhs + WithQuestion :| k₁ : ks' -> do + tV' <- with _O' (k₁ :| ks') v if Eval.conv values _O' tV' then return (VOptional _O') else die OptionalWithTypeMismatch From 5651b80d790342ed5231f703c371d47c40e7f552 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Mar 2025 19:05:37 +0100 Subject: [PATCH 4/4] revert refactor as it fails --- dhall/src/Dhall/TypeCheck.hs | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 2a9fcd8a3..d40434d86 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -1314,25 +1314,6 @@ infer typer = loop VOptional _O' -> do case ks of - -- The old rule was: - -- - -- Γ ⊢ e : Optional T - -- Γ ⊢ v : T' - -- T === T' - -- ────────────────────────────────── - -- Γ ⊢ e with ?.ks… = v : Optional T - -- - -- Here T is _O' and T' = tV'. - -- - -- The new rule is: - -- - -- Γ ⊢ e : Optional T - -- Γ, x : T ⊢ x with ks… = v : T₁ - -- T ≡ T₁ - -- ────────────────────────────────── x ∉ FV(v) - -- Γ ⊢ e with ?.ks… = v : Optional T - -- - -- Here T is _O' and T₁ is tV'. -- (Some x) with ? = v is valid iff the type of x is the same as the type of v. WithQuestion :| [] -> do