From b66de13771b254f5be9739eeb35edf8cdf64c304 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 15:26:08 +0100 Subject: [PATCH 01/26] wip add the functionality of CombineTypes to Combine --- dhall/src/Dhall/TypeCheck.hs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 9c2a30355..7cf42d6a1 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -801,11 +801,15 @@ infer typer = loop Combine _ mk l r -> do _L' <- loop ctx l - let l'' = quote names (eval values l) + let l' = eval values l + + let l'' = quote names l' _R' <- loop ctx r - let r'' = quote names (eval values r) + let r' = eval values r + + let r'' = quote names r' xLs' <- case _L' of VRecord xLs' -> From e07a39ef60ce8f06bb72cc5a0d46ee395f26fdc2 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 15:31:04 +0100 Subject: [PATCH 02/26] wip --- dhall/src/Dhall/TypeCheck.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 7cf42d6a1..6e7264a25 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -814,7 +814,7 @@ infer typer = loop xLs' <- case _L' of VRecord xLs' -> return xLs' - +-- or it can be VConst Type or similar, if we are doing /\ on two record types. _ -> do let _L'' = quote names _L' @@ -832,7 +832,7 @@ infer typer = loop case mk of Nothing -> die (MustCombineARecord '∧' r'' _R'') Just t -> die (InvalidDuplicateField t r _R'') - +-- TODO examine why this `combineTypes` is different from that defined in `CombineTypes _ l r`. let combineTypes xs xLs₀' xRs₀' = do let combine x (VRecord xLs₁') (VRecord xRs₁') = combineTypes (x : xs) xLs₁' xRs₁' From 068d6232893a61a5fc7f4e488d35484162ced479 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 21:44:04 +0100 Subject: [PATCH 03/26] pretty-print //\\ as /\ now globlly --- dhall/src/Dhall/Pretty/Internal.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index fdd545d3c..4b9c7b305 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -432,8 +432,7 @@ combine ASCII = "/\\" combine Unicode = "∧" combineTypes :: CharacterSet -> Text -combineTypes ASCII = "//\\\\" -combineTypes Unicode = "⩓" +combineTypes = combine -- Replace //\\ by /\ as //\\ is now deprecated. prefer :: CharacterSet -> Text prefer ASCII = "//" From bb59a38385d7a5ef19eb28158dd4d5cc36dc5e6b Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 13 Mar 2025 22:27:33 +0100 Subject: [PATCH 04/26] typechecking of record type /\ record type --- dhall/src/Dhall/TypeCheck.hs | 41 ++++++++++++++++++++++++++++-------- 1 file changed, 32 insertions(+), 9 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 6e7264a25..8df8b9bf2 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -811,10 +811,11 @@ infer typer = loop let r'' = quote names r' - xLs' <- case _L' of - VRecord xLs' -> - return xLs' --- or it can be VConst Type or similar, if we are doing /\ on two record types. + leftTypeOrRecord <- case (_L', l') of + (VRecord xLs', _) -> return (Left xLs') + + (VConst cL, VRecord xLs') -> return (Right (cL, xLs')) + _ -> do let _L'' = quote names _L' @@ -822,9 +823,12 @@ infer typer = loop Nothing -> die (MustCombineARecord '∧' l'' _L'') Just t -> die (InvalidDuplicateField t l _L'') - xRs' <- case _R' of - VRecord xRs' -> - return xRs' + -- Make sure both are on the Left (both record values) or on the Right (both record types). + rightTypeOrRecord <- case (leftTypeOrRecord, _R', r') of + (Left _, VRecord xRs', _) -> + return (Left xRs') + + (Right _, VConst cR, VRecord xRs') -> return (Right (cR, xRs')) _ -> do let _R'' = quote names _R' @@ -832,7 +836,7 @@ infer typer = loop case mk of Nothing -> die (MustCombineARecord '∧' r'' _R'') Just t -> die (InvalidDuplicateField t r _R'') --- TODO examine why this `combineTypes` is different from that defined in `CombineTypes _ l r`. + let combineTypes xs xLs₀' xRs₀' = do let combine x (VRecord xLs₁') (VRecord xRs₁') = combineTypes (x : xs) xLs₁' xRs₁' @@ -849,7 +853,26 @@ infer typer = loop return (VRecord xTs) - combineTypes [] xLs' xRs' + let combineTypesCheck xs xLs₀' xRs₀' = do + let combine x (VRecord xLs₁') (VRecord xRs₁') = + combineTypesCheck (x : xs) xLs₁' xRs₁' + + combine x _ _ = + die (FieldTypeCollision (NonEmpty.reverse (x :| xs))) + + let mL = Dhall.Map.toMap xLs₀' + let mR = Dhall.Map.toMap xRs₀' + + Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) + + case (leftTypeOrRecord, rightTypeOrRecord) of + (Left xLs', Left xRs') -> do + combineTypes [] xLs' xRs' + (Right (cL, xLs'), Right (cR, xRs')) -> do + let c = max cL cR + combineTypesCheck [] xLs' xRs' + return (VConst c) + CombineTypes _ l r -> do _L' <- loop ctx l From f7c03e3ba3bc347457a95a18d779b7685a53f669 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 14 Mar 2025 10:55:12 +0100 Subject: [PATCH 05/26] undo the formatting change because tests fail --- dhall/src/Dhall/Pretty/Internal.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dhall/src/Dhall/Pretty/Internal.hs b/dhall/src/Dhall/Pretty/Internal.hs index 4b9c7b305..fdd545d3c 100644 --- a/dhall/src/Dhall/Pretty/Internal.hs +++ b/dhall/src/Dhall/Pretty/Internal.hs @@ -432,7 +432,8 @@ combine ASCII = "/\\" combine Unicode = "∧" combineTypes :: CharacterSet -> Text -combineTypes = combine -- Replace //\\ by /\ as //\\ is now deprecated. +combineTypes ASCII = "//\\\\" +combineTypes Unicode = "⩓" prefer :: CharacterSet -> Text prefer ASCII = "//" From d21abae2a7b02c4c203e7dca4771029bfa988278 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 14 Mar 2025 11:56:41 +0100 Subject: [PATCH 06/26] implement /\ reduction for record types --- dhall/src/Dhall/Eval.hs | 6 ++++++ dhall/src/Dhall/Normalize.hs | 13 +++++++++---- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 73ba65b7a..c0ff76cc6 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -318,6 +318,12 @@ vCombine mk t u = t' (VRecordLit m, VRecordLit m') -> VRecordLit (Map.unionWith (vCombine Nothing) m m') + (VRecord m, u') | null m -> + u' + (t', VRecord m) | null m -> + t' + (VRecord m, VRecord m') -> + VRecord (Map.unionWith (vCombine Nothing) m m') (t', u') -> VCombine mk t' u' diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index c51377dfd..b8610b328 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -548,15 +548,20 @@ normalizeWithM ctx e0 = loop (Syntax.denote e0) kts' = traverse (traverse loop) kts Combine cs mk x y -> decide <$> loop x <*> loop y where + mergeFields (RecordField _ expr _ _) (RecordField _ expr' _ _) = + Syntax.makeRecordField $ decide expr expr' decide (RecordLit m) r | Data.Foldable.null m = r decide l (RecordLit n) | Data.Foldable.null n = l decide (RecordLit m) (RecordLit n) = - RecordLit (Dhall.Map.unionWith f m n) - where - f (RecordField _ expr _ _) (RecordField _ expr' _ _) = - Syntax.makeRecordField $ decide expr expr' + RecordLit (Dhall.Map.unionWith mergeFields m n) + decide (Record m) r | Data.Foldable.null m = + r + decide l (Record n) | Data.Foldable.null n = + l + decide (Record m) (Record n) = + Record (Dhall.Map.unionWith mergeFields m n) decide l r = Combine cs mk l r CombineTypes cs x y -> decide <$> loop x <*> loop y From be4ea3964069e0444cff3c1b30209bb3b9e0fcf8 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 14 Mar 2025 12:22:06 +0100 Subject: [PATCH 07/26] fix isNormalized --- dhall/src/Dhall/Normalize.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/dhall/src/Dhall/Normalize.hs b/dhall/src/Dhall/Normalize.hs index b8610b328..e17d4859e 100644 --- a/dhall/src/Dhall/Normalize.hs +++ b/dhall/src/Dhall/Normalize.hs @@ -954,6 +954,9 @@ isNormalized e0 = loop (Syntax.denote e0) decide (RecordLit m) _ | Data.Foldable.null m = False decide _ (RecordLit n) | Data.Foldable.null n = False decide (RecordLit _) (RecordLit _) = False + decide (Record m) _ | Data.Foldable.null m = False + decide _ (Record n) | Data.Foldable.null n = False + decide (Record _) (Record _) = False decide _ _ = True CombineTypes _ x y -> loop x && loop y && decide x y where From 11a7b3cb3ef45212de5f1e848e4f09099671a90e Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Mon, 17 Mar 2025 17:48:31 +0100 Subject: [PATCH 08/26] add comment --- dhall/src/Dhall/TypeCheck.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 8df8b9bf2..c64bd7976 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -83,6 +83,7 @@ import qualified Dhall.Syntax as Syntax import qualified Dhall.Util import qualified Prettyprinter as Pretty import qualified Prettyprinter.Render.String as Pretty +import qualified Data.Type.Bool as types {-| A type synonym for `Void` @@ -811,6 +812,10 @@ infer typer = loop let r'' = quote names r' + -- The `Combine` operator should now work on record terms and also on record types. + -- If both sides are record terms, we set leftTypeOrRecord and rightTypeOrRecord to (Left record_fields). + -- If both sides are record types, we set both of them to (Right (Type, record_fields)). + -- Then we match the pair (leftTypeOrRecord, rightTypeOrRecord) to make sure we catch errors. leftTypeOrRecord <- case (_L', l') of (VRecord xLs', _) -> return (Left xLs') From 8050d24e226fc93c72d5483a8b39b76d4f882a25 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Mon, 17 Mar 2025 18:10:02 +0100 Subject: [PATCH 09/26] remove wrong import --- dhall/src/Dhall/TypeCheck.hs | 1 - 1 file changed, 1 deletion(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index c64bd7976..efa07f064 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -83,7 +83,6 @@ import qualified Dhall.Syntax as Syntax import qualified Dhall.Util import qualified Prettyprinter as Pretty import qualified Prettyprinter.Render.String as Pretty -import qualified Data.Type.Bool as types {-| A type synonym for `Void` From 8fe9623e98154df4d43c282e9ff9bf4254c79e7c Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 20 Mar 2025 22:29:00 +0100 Subject: [PATCH 10/26] refactor code for clarity --- dhall/src/Dhall/TypeCheck.hs | 67 +++++++++++++++++------------------- 1 file changed, 31 insertions(+), 36 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index efa07f064..792d56f53 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -801,46 +801,22 @@ infer typer = loop Combine _ mk l r -> do _L' <- loop ctx l + let _L'' = quote names _L' + let l' = eval values l let l'' = quote names l' _R' <- loop ctx r + let _R'' = quote names _R' + let r' = eval values r let r'' = quote names r' -- The `Combine` operator should now work on record terms and also on record types. - -- If both sides are record terms, we set leftTypeOrRecord and rightTypeOrRecord to (Left record_fields). - -- If both sides are record types, we set both of them to (Right (Type, record_fields)). - -- Then we match the pair (leftTypeOrRecord, rightTypeOrRecord) to make sure we catch errors. - leftTypeOrRecord <- case (_L', l') of - (VRecord xLs', _) -> return (Left xLs') - - (VConst cL, VRecord xLs') -> return (Right (cL, xLs')) - - _ -> do - let _L'' = quote names _L' - - case mk of - Nothing -> die (MustCombineARecord '∧' l'' _L'') - Just t -> die (InvalidDuplicateField t l _L'') - - -- Make sure both are on the Left (both record values) or on the Right (both record types). - rightTypeOrRecord <- case (leftTypeOrRecord, _R', r') of - (Left _, VRecord xRs', _) -> - return (Left xRs') - - (Right _, VConst cR, VRecord xRs') -> return (Right (cR, xRs')) - - _ -> do - let _R'' = quote names _R' - - case mk of - Nothing -> die (MustCombineARecord '∧' r'' _R'') - Just t -> die (InvalidDuplicateField t r _R'') - + -- We will use combineTypes or combineTypesCheck below as needed for each case. let combineTypes xs xLs₀' xRs₀' = do let combine x (VRecord xLs₁') (VRecord xRs₁') = combineTypes (x : xs) xLs₁' xRs₁' @@ -869,13 +845,32 @@ infer typer = loop Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) - case (leftTypeOrRecord, rightTypeOrRecord) of - (Left xLs', Left xRs') -> do - combineTypes [] xLs' xRs' - (Right (cL, xLs'), Right (cR, xRs')) -> do - let c = max cL cR - combineTypesCheck [] xLs' xRs' - return (VConst c) + -- If both sides of `Combine` are record terms, we use combineTypes to figure out the resulting type. + -- If both sides are record types, we use combineTypesCheck and then return the upper bound of two types. + -- Otherwise there is a type error. + case (_L', l', _R', r') of + (VRecord xLs', _, VRecord xRs', _) -> do + combineTypes [] xLs' xRs' + + (VConst cL, VRecord xLs', VConst cR, VRecord xRs') -> do + let c = max cL cR + combineTypesCheck [] xLs' xRs' + return (VConst c) + + (_, _, VRecord _, _) -> do + case mk of + Nothing -> die (MustCombineARecord '∧' l'' _L'') + Just t -> die (InvalidDuplicateField t l _L'') + + (_, _, VConst _, _) -> do + case mk of + Nothing -> die (MustCombineARecord '∧' l'' _L'') + Just t -> die (InvalidDuplicateField t l _L'') + + _ -> do + case mk of + Nothing -> die (MustCombineARecord '∧' r'' _R'') + Just t -> die (InvalidDuplicateField t r _R'') CombineTypes _ l r -> do From 20dfebdec5c6a0a64ac4a7065546bec28901052c Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 7 May 2025 15:50:50 +0200 Subject: [PATCH 11/26] bump ci From 5933b6a2f7a62cffff051b32c13cffe9281116d2 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 7 May 2025 19:07:05 +0200 Subject: [PATCH 12/26] bump ci From 189d572c48cee2c3ee14d07abc360d35748f8386 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 15 May 2025 15:16:37 +0200 Subject: [PATCH 13/26] bump ci From 0bcc84d776fc4897b9be3fe9f758ee6d5b242d38 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 16 May 2025 15:06:06 +0200 Subject: [PATCH 14/26] bump ci From 0ecadb1d10b6a49abc42eb2e059533eceded80d6 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 16 May 2025 15:19:53 +0200 Subject: [PATCH 15/26] bump ci From 400549eb803fa974a3167093cd68fc43a9bad4b4 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Sat, 17 May 2025 15:19:58 +0200 Subject: [PATCH 16/26] bump ci From 43a8741c1afc0f48d0b608874e75e721f76991b4 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Sat, 17 May 2025 18:58:22 +0200 Subject: [PATCH 17/26] bump ci From 5f51a3f9f2c84ae88c8ade37feaddcc87652be8a Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Sun, 18 May 2025 10:58:43 +0200 Subject: [PATCH 18/26] bump ci From 7864ec9b1a4116eec12485db61c169085c3c8e3d Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 19 Jun 2025 14:17:43 +0200 Subject: [PATCH 19/26] bump ci From d7b782c6d8c966316eccbcdd6ce647fb66388bcf Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 19 Jun 2025 22:26:43 +0200 Subject: [PATCH 20/26] refactor to use combineTypesCheckingForFieldCollisions outside of loop matches --- dhall/src/Dhall/TypeCheck.hs | 46 ++++++++++++++---------------------- 1 file changed, 18 insertions(+), 28 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index b0b9bc3ee..4f708610f 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -798,6 +798,7 @@ infer typer = loop Max c <- fmap Foldable.fold (Dhall.Map.unorderedTraverseWithKey process xTs) return (VConst c) + Combine _ mk l r -> do _L' <- loop ctx l @@ -833,20 +834,8 @@ infer typer = loop return (VRecord xTs) - let combineTypesCheck xs xLs₀' xRs₀' = do - let combine x (VRecord xLs₁') (VRecord xRs₁') = - combineTypesCheck (x : xs) xLs₁' xRs₁' - - combine x _ _ = - die (FieldTypeCollision (NonEmpty.reverse (x :| xs))) - - let mL = Dhall.Map.toMap xLs₀' - let mR = Dhall.Map.toMap xRs₀' - - Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) - - -- If both sides of `Combine` are record terms, we use combineTypes to figure out the resulting type. - -- If both sides are record types, we use combineTypesCheck and then return the upper bound of two types. + -- If both sides of `Combine` are record terms (and their types match VRecord _), we use combineTypes to figure out the resulting type. + -- If both sides are record types (and their types match VConst _), we run combineTypesCheckingForFieldCollisions and then return the upper bound of the two types. -- Otherwise there is a type error. case (_L', l', _R', r') of (VRecord xLs', _, VRecord xRs', _) -> do @@ -854,7 +843,7 @@ infer typer = loop (VConst cL, VRecord xLs', VConst cR, VRecord xRs') -> do let c = max cL cR - combineTypesCheck [] xLs' xRs' + combineTypesCheckingForFieldCollisions [] xLs' xRs' return (VConst c) (_, _, VRecord _, _) -> do @@ -904,19 +893,7 @@ infer typer = loop VRecord xRs' -> return xRs' _ -> die (CombineTypesRequiresRecordType r r'') - let combineTypes xs xLs₀' xRs₀' = do - let combine x (VRecord xLs₁') (VRecord xRs₁') = - combineTypes (x : xs) xLs₁' xRs₁' - - combine x _ _ = - die (FieldTypeCollision (NonEmpty.reverse (x :| xs))) - - let mL = Dhall.Map.toMap xLs₀' - let mR = Dhall.Map.toMap xRs₀' - - Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) - - combineTypes [] xLs' xRs' + combineTypesCheckingForFieldCollisions [] xLs' xRs' return (VConst c) @@ -1386,6 +1363,19 @@ infer typer = loop quote ns value = Dhall.Core.renote (Eval.quote ns value) + combineTypesCheckingForFieldCollisions xs xLs₀' xRs₀' = Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) + where + combine x (VRecord xLs₁') (VRecord xRs₁') = + combineTypesCheckingForFieldCollisions (x : xs) xLs₁' xRs₁' + + combine x _ _ = + die (FieldTypeCollision (NonEmpty.reverse (x :| xs))) + + mL = Dhall.Map.toMap xLs₀' + mR = Dhall.Map.toMap xRs₀' + + + {-| `typeOf` is the same as `typeWith` with an empty context, meaning that the expression must be closed (i.e. no free variables), otherwise type-checking will fail. From 53a5a3d4834bd1a09f94f0303b37e85d37c19a89 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 19 Jun 2025 22:37:43 +0200 Subject: [PATCH 21/26] minor rewrite --- dhall/src/Dhall/TypeCheck.hs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 4f708610f..e09a64f8e 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -816,8 +816,8 @@ infer typer = loop let r'' = quote names r' - -- The `Combine` operator should now work on record terms and also on record types. - -- We will use combineTypes or combineTypesCheck below as needed for each case. + -- The `Combine` operator needs to work on record terms and also on record types. + -- We will use combineTypes or recordTypesHaveNoFieldCollisions below as needed for each case. let combineTypes xs xLs₀' xRs₀' = do let combine x (VRecord xLs₁') (VRecord xRs₁') = combineTypes (x : xs) xLs₁' xRs₁' @@ -835,15 +835,15 @@ infer typer = loop return (VRecord xTs) -- If both sides of `Combine` are record terms (and their types match VRecord _), we use combineTypes to figure out the resulting type. - -- If both sides are record types (and their types match VConst _), we run combineTypesCheckingForFieldCollisions and then return the upper bound of the two types. + -- If both sides are record types (and their kinds match VConst _), we check recordTypesHaveNoFieldCollisions and then return the upper bound of the two types. -- Otherwise there is a type error. case (_L', l', _R', r') of - (VRecord xLs', _, VRecord xRs', _) -> do + (VRecord xLs', _, VRecord xRs', _) -> do -- Both arguments are record terms. combineTypes [] xLs' xRs' - (VConst cL, VRecord xLs', VConst cR, VRecord xRs') -> do + (VConst cL, VRecord xLs', VConst cR, VRecord xRs') -> do -- Both arguments are record types. let c = max cL cR - combineTypesCheckingForFieldCollisions [] xLs' xRs' + recordTypesHaveNoFieldCollisions [] xLs' xRs' return (VConst c) (_, _, VRecord _, _) -> do @@ -893,7 +893,7 @@ infer typer = loop VRecord xRs' -> return xRs' _ -> die (CombineTypesRequiresRecordType r r'') - combineTypesCheckingForFieldCollisions [] xLs' xRs' + recordTypesHaveNoFieldCollisions [] xLs' xRs' return (VConst c) @@ -1363,10 +1363,10 @@ infer typer = loop quote ns value = Dhall.Core.renote (Eval.quote ns value) - combineTypesCheckingForFieldCollisions xs xLs₀' xRs₀' = Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) + recordTypesHaveNoFieldCollisions xs xLs₀' xRs₀' = Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) where combine x (VRecord xLs₁') (VRecord xRs₁') = - combineTypesCheckingForFieldCollisions (x : xs) xLs₁' xRs₁' + recordTypesHaveNoFieldCollisions (x : xs) xLs₁' xRs₁' combine x _ _ = die (FieldTypeCollision (NonEmpty.reverse (x :| xs))) From df0330ce696852e6a49e2fb5f92cb4d26f2f9880 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Thu, 19 Jun 2025 23:16:22 +0200 Subject: [PATCH 22/26] Add a better error message for the case of /\ on record terms or types --- dhall/src/Dhall/TypeCheck.hs | 81 +++++++++++++++++++++++++++++++----- 1 file changed, 70 insertions(+), 11 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index e09a64f8e..5fc2a82e0 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -846,20 +846,16 @@ infer typer = loop recordTypesHaveNoFieldCollisions [] xLs' xRs' return (VConst c) - (_, _, VRecord _, _) -> do + (VRecord _, _, _, _) -> do -- The left argument is a record term, the right argument is not. The error is in the right argument. case mk of - Nothing -> die (MustCombineARecord '∧' l'' _L'') - Just t -> die (InvalidDuplicateField t l _L'') + Nothing -> die (MustCombineARecord '∧' r'' _R'') + Just t -> die (InvalidDuplicateField t r _R'') - (_, _, VConst _, _) -> do - case mk of - Nothing -> die (MustCombineARecord '∧' l'' _L'') - Just t -> die (InvalidDuplicateField t l _L'') + (VConst _, VRecord _, _, _) -> do -- The left argument is a record type, the right argument is not. The error is in the right argument. + die (CombineTypesRequiresRecordType r r'') - _ -> do - case mk of - Nothing -> die (MustCombineARecord '∧' r'' _R'') - Just t -> die (InvalidDuplicateField t r _R'') + _ -> do -- The error is in the left argument: it must be either a record term or a record type, but it is neither. + die (MustCombineARecordOrRecordType '∧' l l'') CombineTypes _ l r -> do @@ -1405,6 +1401,7 @@ data TypeMessage s a | ListAppendMismatch (Expr s a) (Expr s a) | MustUpdateARecord (Expr s a) (Expr s a) (Expr s a) | MustCombineARecord Char (Expr s a) (Expr s a) + | MustCombineARecordOrRecordType Char (Expr s a) (Expr s a) | InvalidDuplicateField Text (Expr s a) (Expr s a) | InvalidRecordCompletion Text (Expr s a) | CompletionSchemaMustBeARecord (Expr s a) (Expr s a) @@ -2875,6 +2872,66 @@ prettyTypeMessage (MustCombineARecord c expression typeExpression) = where op = pretty c +prettyTypeMessage (MustCombineARecordOrRecordType c expression typeExpression) = + ErrorMessages {..} + where + action = "combine" + short = "You can only " <> action <> " records or record types" + + hints = emptyRecordTypeHint expression + + long = + "Explanation: You can " <> action <> " records or record types using the ❰" <> op <> "❱ operator, like this:\n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────┐ \n\ + \ │ { foo = 1, bar = \"ABC\" } " <> op <> " { baz = True } │ \n\ + \ └───────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────┐ \n\ + \ │ { foo : Bool, bar : Text } " <> op <> " { baz : Bool } │ \n\ + \ └───────────────────────────────────────────┘ \n\ + \ \n\ + \ \n\ + \... but you cannot " <> action <> " values that are neither records nor record types.\n\ + \ \n\ + \For example, the following expressions are " <> _NOT <> " valid: \n\ + \ \n\ + \ \n\ + \ ┌──────────────────────────────┐ \n\ + \ │ 1 " <> op <> " { foo = 1, bar = \"ABC\" } │ \n\ + \ └──────────────────────────────┘ \n\ + \ ⇧ \n\ + \ Invalid: This is not a record and not a record type \n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────┐ \n\ + \ │ { foo = 1, bar = \"ABC\" } " <> op <> " { baz : Bool } │ \n\ + \ └───────────────────────────────────────────┘ \n\ + \ ⇧ \n\ + \ Invalid: This is a record type and not a record\n\ + \ \n\ + \ \n\ + \ ┌───────────────────────────────────────────┐ \n\ + \ │ < baz : Bool > " <> op <> " { foo = 1, bar = \"ABC\" } │ \n\ + \ └───────────────────────────────────────────┘ \n\ + \ ⇧ \n\ + \ Invalid: This is a union type and not a record \n\ + \ \n\ + \ \n\ + \────────────────────────────────────────────────────────────────────────────────\n\ + \ \n\ + \You supplied this expression as one of the arguments: \n\ + \ \n\ + \" <> insert expression <> "\n\ + \ \n\ + \... which is not a record or a record type, but is actually a: \n\ + \ \n\ + \" <> insert typeExpression <> "\n" + where + op = pretty c + prettyTypeMessage (InvalidDuplicateField k expr0 expr1) = ErrorMessages {..} where @@ -4921,6 +4978,8 @@ messageExpressions f m = case m of MustUpdateARecord <$> f a <*> f b <*> f c MustCombineARecord a b c -> MustCombineARecord <$> pure a <*> f b <*> f c + MustCombineARecordOrRecordType a b c -> + MustCombineARecordOrRecordType <$> pure a <*> f b <*> f c InvalidRecordCompletion a l -> InvalidRecordCompletion a <$> f l CompletionSchemaMustBeARecord l r -> From aa6fd30312ec7b2fa0b44241b93d612c7c871ef7 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 20 Jun 2025 15:16:42 +0200 Subject: [PATCH 23/26] implement better error messages --- dhall/src/Dhall/TypeCheck.hs | 59 ++++++++++++++++++++---------------- 1 file changed, 33 insertions(+), 26 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 5fc2a82e0..99a98dd56 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -843,19 +843,24 @@ infer typer = loop (VConst cL, VRecord xLs', VConst cR, VRecord xRs') -> do -- Both arguments are record types. let c = max cL cR - recordTypesHaveNoFieldCollisions [] xLs' xRs' + recordTypesHaveNoFieldCollisions '∧' [] xLs' xRs' return (VConst c) - (VRecord _, _, _, _) -> do -- The left argument is a record term, the right argument is not. The error is in the right argument. + (VRecord _, _, _, _) -> do -- The left argument is a record term, the right argument is not. We report the error in the right argument. case mk of Nothing -> die (MustCombineARecord '∧' r'' _R'') Just t -> die (InvalidDuplicateField t r _R'') - (VConst _, VRecord _, _, _) -> do -- The left argument is a record type, the right argument is not. The error is in the right argument. - die (CombineTypesRequiresRecordType r r'') + (_, _, VRecord _, _) -> do -- The right argument is a record term, the left argument is not. We report the error in the left argument. + case mk of + Nothing -> die (MustCombineARecord '∧' l'' _L'') + Just t -> die (InvalidDuplicateField t l _L'') + + (VConst _, VRecord _, _, _) -> do -- The left argument is a record type, the right argument is not. We report the error in the right argument. + die (MustCombineRecordsOrRecordTypes '∧' r r'') - _ -> do -- The error is in the left argument: it must be either a record term or a record type, but it is neither. - die (MustCombineARecordOrRecordType '∧' l l'') + _ -> do -- The error is in the left argument: it must be either a record term or a record type, but it is neither. We report the error in the left argument. + die (MustCombineRecordsOrRecordTypes '∧' l l'') CombineTypes _ l r -> do @@ -889,7 +894,7 @@ infer typer = loop VRecord xRs' -> return xRs' _ -> die (CombineTypesRequiresRecordType r r'') - recordTypesHaveNoFieldCollisions [] xLs' xRs' + recordTypesHaveNoFieldCollisions '⩓' [] xLs' xRs' return (VConst c) @@ -1359,13 +1364,13 @@ infer typer = loop quote ns value = Dhall.Core.renote (Eval.quote ns value) - recordTypesHaveNoFieldCollisions xs xLs₀' xRs₀' = Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) + recordTypesHaveNoFieldCollisions c xs xLs₀' xRs₀' = Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR) where combine x (VRecord xLs₁') (VRecord xRs₁') = - recordTypesHaveNoFieldCollisions (x : xs) xLs₁' xRs₁' + recordTypesHaveNoFieldCollisions c (x : xs) xLs₁' xRs₁' combine x _ _ = - die (FieldTypeCollision (NonEmpty.reverse (x :| xs))) + die (FieldTypeCollision c (NonEmpty.reverse (x :| xs))) mL = Dhall.Map.toMap xLs₀' mR = Dhall.Map.toMap xRs₀' @@ -1401,7 +1406,7 @@ data TypeMessage s a | ListAppendMismatch (Expr s a) (Expr s a) | MustUpdateARecord (Expr s a) (Expr s a) (Expr s a) | MustCombineARecord Char (Expr s a) (Expr s a) - | MustCombineARecordOrRecordType Char (Expr s a) (Expr s a) + | MustCombineRecordsOrRecordTypes Char (Expr s a) (Expr s a) | InvalidDuplicateField Text (Expr s a) (Expr s a) | InvalidRecordCompletion Text (Expr s a) | CompletionSchemaMustBeARecord (Expr s a) (Expr s a) @@ -1409,7 +1414,7 @@ data TypeMessage s a | RecordTypeMismatch Const Const (Expr s a) (Expr s a) | DuplicateFieldCannotBeMerged (NonEmpty Text) | FieldCollision (NonEmpty Text) - | FieldTypeCollision (NonEmpty Text) + | FieldTypeCollision Char (NonEmpty Text) | MustMergeARecord (Expr s a) (Expr s a) | MustMergeUnionOrOptional (Expr s a) (Expr s a) | MustMapARecord (Expr s a) (Expr s a) @@ -2872,16 +2877,16 @@ prettyTypeMessage (MustCombineARecord c expression typeExpression) = where op = pretty c -prettyTypeMessage (MustCombineARecordOrRecordType c expression typeExpression) = +prettyTypeMessage (MustCombineRecordsOrRecordTypes c expression typeExpression) = ErrorMessages {..} where action = "combine" - short = "You can only " <> action <> " records or record types" + short = "You can only " <> action <> " two records or two record types" hints = emptyRecordTypeHint expression long = - "Explanation: You can " <> action <> " records or record types using the ❰" <> op <> "❱ operator, like this:\n\ + "Explanation: You can " <> action <> " two records or two record types using the ❰" <> op <> "❱ operator, like this:\n\ \ \n\ \ \n\ \ ┌───────────────────────────────────────────┐ \n\ @@ -2894,7 +2899,7 @@ prettyTypeMessage (MustCombineARecordOrRecordType c expression typeExpression) = \ └───────────────────────────────────────────┘ \n\ \ \n\ \ \n\ - \... but you cannot " <> action <> " values that are neither records nor record types.\n\ + \... but you cannot " <> action <> " values that are not both records and not both record types.\n\ \ \n\ \For example, the following expressions are " <> _NOT <> " valid: \n\ \ \n\ @@ -2910,7 +2915,7 @@ prettyTypeMessage (MustCombineARecordOrRecordType c expression typeExpression) = \ │ { foo = 1, bar = \"ABC\" } " <> op <> " { baz : Bool } │ \n\ \ └───────────────────────────────────────────┘ \n\ \ ⇧ \n\ - \ Invalid: This is a record type and not a record\n\ + \ Invalid: cannot combine a record and a record type\n\ \ \n\ \ \n\ \ ┌───────────────────────────────────────────┐ \n\ @@ -3224,19 +3229,21 @@ prettyTypeMessage (FieldCollision ks) = ErrorMessages {..} where txt0 = insert (toPath ks) -prettyTypeMessage (FieldTypeCollision ks) = ErrorMessages {..} +prettyTypeMessage (FieldTypeCollision c ks) = ErrorMessages {..} where + op = pretty c + short = "Field type collision on: " <> pretty (toPath ks) hints = [] long = - "Explanation: You can recursively merge record types using the ❰⩓❱ operator, like\n\ + "Explanation: You can recursively merge record types using the ❰" <> op <> "❱ operator, like\n\ \this: \n\ \ \n\ \ \n\ \ ┌───────────────────────┐ \n\ - \ │ { x : A } ⩓ { y : B } │ \n\ + \ │ { x : A } " <> op <> " { y : B } │ \n\ \ └───────────────────────┘ \n\ \ \n\ \ \n\ @@ -3247,7 +3254,7 @@ prettyTypeMessage (FieldTypeCollision ks) = ErrorMessages {..} \ \n\ \ \n\ \ ┌────────────────────────────────┐ \n\ - \ │ { x : Natural } ⩓ { x : Bool } │ Invalid: The ❰x❱ fields \"collide\" \n\ + \ │ { x : Natural } " <> op <> " { x : Bool } │ Invalid: The ❰x❱ fields \"collide\" \n\ \ └────────────────────────────────┘ because they cannot be merged \n\ \ \n\ \ \n\ @@ -3255,7 +3262,7 @@ prettyTypeMessage (FieldTypeCollision ks) = ErrorMessages {..} \ \n\ \ \n\ \ ┌────────────────────────────────────────────────┐ Valid: The ❰x❱ field \n\ - \ │ { x : { y : Bool } } ⩓ { x : { z : Natural } } │ types don't collide and \n\ + \ │ { x : { y : Bool } } " <> op <> " { x : { z : Natural } } │ types don't collide and \n\ \ └────────────────────────────────────────────────┘ can be merged \n\ \ \n\ \ \n\ @@ -4978,8 +4985,8 @@ messageExpressions f m = case m of MustUpdateARecord <$> f a <*> f b <*> f c MustCombineARecord a b c -> MustCombineARecord <$> pure a <*> f b <*> f c - MustCombineARecordOrRecordType a b c -> - MustCombineARecordOrRecordType <$> pure a <*> f b <*> f c + MustCombineRecordsOrRecordTypes a b c -> + MustCombineRecordsOrRecordTypes <$> pure a <*> f b <*> f c InvalidRecordCompletion a l -> InvalidRecordCompletion a <$> f l CompletionSchemaMustBeARecord l r -> @@ -4992,8 +4999,8 @@ messageExpressions f m = case m of pure (DuplicateFieldCannotBeMerged a) FieldCollision a -> pure (FieldCollision a) - FieldTypeCollision a -> - pure (FieldTypeCollision a) + FieldTypeCollision c a -> + pure (FieldTypeCollision c a) MustMergeARecord a b -> MustMergeARecord <$> f a <*> f b MustMergeUnionOrOptional a b -> From c942a3d3f19aebe792c5619059c00ad2ed70bd33 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 20 Jun 2025 17:56:22 +0200 Subject: [PATCH 24/26] wip adding unit tests for CombineTypes feature --- dhall/src/Dhall/TypeCheck.hs | 4 +-- dhall/tests/Dhall/Test/Regression.hs | 40 ++++++++++++++++++++++++++++ 2 files changed, 42 insertions(+), 2 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 99a98dd56..2fc57b4c3 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -2971,8 +2971,8 @@ prettyTypeMessage (InvalidDuplicateField k expr0 expr1) = \ └────────────────────────────────────────────────┘ \n\ \ \n\ \ \n\ - \However, this implies that both fields must be records since the ❰∧❱ operator \n\ - \cannot merge non-record values. For example, these expressions are not valid: \n\ + \However, this implies that both fields must be records or record types since the\n\ + \ ❰∧❱ operator cannot merge other values. Examples of invalid expressions are: \n\ \ \n\ \ \n\ \ ┌──────────────────┐ \n\ diff --git a/dhall/tests/Dhall/Test/Regression.hs b/dhall/tests/Dhall/Test/Regression.hs index f03817805..f1db92b80 100644 --- a/dhall/tests/Dhall/Test/Regression.hs +++ b/dhall/tests/Dhall/Test/Regression.hs @@ -13,6 +13,7 @@ import Dhall.Parser (SourcedException (..), Src) import Dhall.TypeCheck (TypeError) import Test.Tasty (TestTree) import Test.Tasty.HUnit ((@?=)) +import Data.Text (Text) import qualified Control.Exception import qualified Data.Text.IO @@ -31,6 +32,15 @@ import qualified Prettyprinter.Render.Text import qualified System.Timeout import qualified Test.Tasty import qualified Test.Tasty.HUnit +import Dhall.TypeCheck (TypeError(typeMessage)) +import Dhall.TypeCheck (prettyTypeMessage) +import qualified Data.Text as Text +import Dhall.TypeCheck (short) +import qualified Data.List as List +import qualified Prettyprinter as Pretty +import Prettyprinter.Render.Text (renderStrict) +import Dhall.TypeCheck (ErrorMessages(long)) + tests :: TestTree tests = @@ -57,6 +67,7 @@ tests = , typeChecking2 , unnamedFields , trailingSpaceAfterStringLiterals + , combineTypes ] data Foo = Foo Integer Bool | Bar Bool Bool Bool | Baz Integer Integer @@ -325,3 +336,32 @@ trailingSpaceAfterStringLiterals = -- (Yes, I did get this wrong at some point) _ <- Util.code "(''\nABC'' ++ \"DEF\" )" return () ) + +hasTypeErrorWithMessage :: Text -> [ Text] -> IO () +hasTypeErrorWithMessage dhallCode expectedErrorMessageSubstrings = do + let handler :: Dhall.TypeCheck.TypeError Src Void -> IO (Bool, Maybe (Dhall.TypeCheck.TypeMessage Src Void)) + handler e = return (True, Just (typeMessage e)) + + let typeCheck = do + _ <- Util.code dhallCode + return (False, Nothing) + + (b, Just actualTypeError) <- Control.Exception.handle handler typeCheck + Test.Tasty.HUnit.assertBool "The expression should not type-check" b + let message = prettyTypeMessage actualTypeError + -- Concatenate the short and the long doc strings in an ErrorMessages structure: + let concatenateAllDocStrings m = Pretty.vsep [short m, long m] + -- Whether `message` has `s` as a substring: + let haveSubstring :: Text -> Bool + haveSubstring text = Text.isInfixOf text (renderStrict (Pretty.layoutPretty Pretty.defaultLayoutOptions (concatenateAllDocStrings message))) + let haveAllSubstrings = List.all haveSubstring expectedErrorMessageSubstrings + + Test.Tasty.HUnit.assertBool "The error message should contain all expected substrings" haveAllSubstrings + + return () + +combineTypes :: TestTree +combineTypes = Test.Tasty.HUnit.testCase "Combine Types" (do + hasTypeErrorWithMessage "{a : Bool } /\\ { b = 0 }" ["You can only combine records"] + hasTypeErrorWithMessage "{a : Bool } /\\ { a : Natural }" ["Field type collision on: a", "{ x : A } ∧ { y : B }"] + ) From 87845fadc212c8adc11b4a782c770255b576ac40 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Fri, 20 Jun 2025 22:16:31 +0200 Subject: [PATCH 25/26] add unit tests for new error messages --- dhall/src/Dhall/TypeCheck.hs | 53 ++++++++++++++++------------ dhall/tests/Dhall/Test/Regression.hs | 32 ++++++++++++----- 2 files changed, 54 insertions(+), 31 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index 2fc57b4c3..f49c67eb5 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -856,11 +856,8 @@ infer typer = loop Nothing -> die (MustCombineARecord '∧' l'' _L'') Just t -> die (InvalidDuplicateField t l _L'') - (VConst _, VRecord _, _, _) -> do -- The left argument is a record type, the right argument is not. We report the error in the right argument. - die (MustCombineRecordsOrRecordTypes '∧' r r'') - - _ -> do -- The error is in the left argument: it must be either a record term or a record type, but it is neither. We report the error in the left argument. - die (MustCombineRecordsOrRecordTypes '∧' l l'') + _ -> do -- One of the arguments is a record type, but the other argument is not. + die (MustCombineRecordsOrRecordTypes l'' _L'' r _R'') CombineTypes _ l r -> do @@ -1406,7 +1403,7 @@ data TypeMessage s a | ListAppendMismatch (Expr s a) (Expr s a) | MustUpdateARecord (Expr s a) (Expr s a) (Expr s a) | MustCombineARecord Char (Expr s a) (Expr s a) - | MustCombineRecordsOrRecordTypes Char (Expr s a) (Expr s a) + | MustCombineRecordsOrRecordTypes (Expr s a) (Expr s a) (Expr s a) (Expr s a) | InvalidDuplicateField Text (Expr s a) (Expr s a) | InvalidRecordCompletion Text (Expr s a) | CompletionSchemaMustBeARecord (Expr s a) (Expr s a) @@ -2821,7 +2818,7 @@ prettyTypeMessage (MustCombineARecord c expression typeExpression) = '∧' -> "combine" _ -> "override" - short = "You can only " <> action <> " records" + short = "You can only " <> action <> " a record with another record" hints = emptyRecordTypeHint expression @@ -2839,7 +2836,7 @@ prettyTypeMessage (MustCombineARecord c expression typeExpression) = \ └─────────────────────────────────────────────┘ \n\ \ \n\ \ \n\ - \... but you cannot " <> action <> " values that are not records. \n\ + \... but you cannot " <> action <> " a record and a value that is not a record. \n\ \ \n\ \For example, the following expressions are " <> _NOT <> " valid: \n\ \ \n\ @@ -2877,29 +2874,31 @@ prettyTypeMessage (MustCombineARecord c expression typeExpression) = where op = pretty c -prettyTypeMessage (MustCombineRecordsOrRecordTypes c expression typeExpression) = +prettyTypeMessage (MustCombineRecordsOrRecordTypes e1 t1 e2 t2) = ErrorMessages {..} where action = "combine" short = "You can only " <> action <> " two records or two record types" - hints = emptyRecordTypeHint expression + hints = emptyRecordTypeHint e1 ++ emptyRecordTypeHint e2 long = - "Explanation: You can " <> action <> " two records or two record types using the ❰" <> op <> "❱ operator, like this:\n\ - \ \n\ + "Explanation: You can " <> action <> " two records or two record types using the ❰" <> op <> "❱ |\n\ + \ operator like this: |\n\ + \ |\n\ \ \n\ \ ┌───────────────────────────────────────────┐ \n\ \ │ { foo = 1, bar = \"ABC\" } " <> op <> " { baz = True } │ \n\ \ └───────────────────────────────────────────┘ \n\ \ \n\ \ \n\ - \ ┌───────────────────────────────────────────┐ \n\ + \ ┌─────────────────────────────────────────────┐ \n\ \ │ { foo : Bool, bar : Text } " <> op <> " { baz : Bool } │ \n\ - \ └───────────────────────────────────────────┘ \n\ + \ └─────────────────────────────────────────────┘ \n\ \ \n\ \ \n\ - \... but you cannot " <> action <> " values that are not both records and not both record types.\n\ + \... but you cannot " <> action <> " values that are not both records \n\ + \ and not both record types. \n\ \ \n\ \For example, the following expressions are " <> _NOT <> " valid: \n\ \ \n\ @@ -2927,15 +2926,25 @@ prettyTypeMessage (MustCombineRecordsOrRecordTypes c expression typeExpression) \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ \ \n\ - \You supplied this expression as one of the arguments: \n\ + \You supplied this expression as the first argument: \n\ \ \n\ - \" <> insert expression <> "\n\ + \" <> insert e1 <> "\n\ \ \n\ - \... which is not a record or a record type, but is actually a: \n\ + \... which has type: \n\ \ \n\ - \" <> insert typeExpression <> "\n" + \" <> insert t1 <> "\n\ + \ \n\ + \You supplied this expression as the second argument: \n\ + \ \n\ + \" <> insert e2 <> "\n\ + \ \n\ + \... which has type: \n\ + \ \n\ + \" <> insert t2 <> "\n\ + \ \n\ + \At least one of these arguments is neither a record type nor a record. \n" where - op = pretty c + op = pretty '∧' -- This message is only for type errors while using ∧. prettyTypeMessage (InvalidDuplicateField k expr0 expr1) = ErrorMessages {..} @@ -4985,8 +4994,8 @@ messageExpressions f m = case m of MustUpdateARecord <$> f a <*> f b <*> f c MustCombineARecord a b c -> MustCombineARecord <$> pure a <*> f b <*> f c - MustCombineRecordsOrRecordTypes a b c -> - MustCombineRecordsOrRecordTypes <$> pure a <*> f b <*> f c + MustCombineRecordsOrRecordTypes a b c d -> + MustCombineRecordsOrRecordTypes <$> f a <*> f b <*> f c <*> f d InvalidRecordCompletion a l -> InvalidRecordCompletion a <$> f l CompletionSchemaMustBeARecord l r -> diff --git a/dhall/tests/Dhall/Test/Regression.hs b/dhall/tests/Dhall/Test/Regression.hs index f1db92b80..176c9fd5d 100644 --- a/dhall/tests/Dhall/Test/Regression.hs +++ b/dhall/tests/Dhall/Test/Regression.hs @@ -347,21 +347,35 @@ hasTypeErrorWithMessage dhallCode expectedErrorMessageSubstrings = do return (False, Nothing) (b, Just actualTypeError) <- Control.Exception.handle handler typeCheck - Test.Tasty.HUnit.assertBool "The expression should not type-check" b + Test.Tasty.HUnit.assertBool ("The expression " <> Text.unpack dhallCode <> " should not type-check") b let message = prettyTypeMessage actualTypeError -- Concatenate the short and the long doc strings in an ErrorMessages structure: let concatenateAllDocStrings m = Pretty.vsep [short m, long m] - -- Whether `message` has `s` as a substring: + -- Whether `message` has `text` as a substring: let haveSubstring :: Text -> Bool - haveSubstring text = Text.isInfixOf text (renderStrict (Pretty.layoutPretty Pretty.defaultLayoutOptions (concatenateAllDocStrings message))) + haveSubstring text = Text.isInfixOf text (renderStrict (Pretty.layoutPretty Pretty.defaultLayoutOptions (concatenateAllDocStrings message))) let haveAllSubstrings = List.all haveSubstring expectedErrorMessageSubstrings - Test.Tasty.HUnit.assertBool "The error message should contain all expected substrings" haveAllSubstrings - + Test.Tasty.HUnit.assertBool ("The error message for " <> Text.unpack dhallCode <> " should contain all expected substrings") haveAllSubstrings return () +-- Verify that each of the expressions fails to type-check and produces a diagnostic text that contains each of the given substrings. combineTypes :: TestTree -combineTypes = Test.Tasty.HUnit.testCase "Combine Types" (do - hasTypeErrorWithMessage "{a : Bool } /\\ { b = 0 }" ["You can only combine records"] - hasTypeErrorWithMessage "{a : Bool } /\\ { a : Natural }" ["Field type collision on: a", "{ x : A } ∧ { y : B }"] - ) +combineTypes = Test.Tasty.HUnit.testCase "Combine / Combine Types error messages" (do + hasTypeErrorWithMessage "{ a : Bool } ∧ { b = 0 }" ["You can only combine a record with another record", "∧", "↳ { a : Bool }", "which is not a record"] + hasTypeErrorWithMessage "{ a : Bool } ∧ { a : Natural }" ["Field type collision on: a", "{ x : A } ∧ { y : B }"] + hasTypeErrorWithMessage "{ a = 0 } ∧ { b : Natural }" ["You can only combine a record with another record", "∧", "↳ { b : Natural }", "which is not a record"] + hasTypeErrorWithMessage "{ a = 0 } ∧ { a : Natural }" ["You can only combine a record with another record", "∧", "↳ { a : Natural }", "which is not a record"] + hasTypeErrorWithMessage "{ a : Bool } ∧ { a = 0 }" ["You can only combine a record with another record", "∧", "↳ { a : Bool }", "which is not a record"] + hasTypeErrorWithMessage "{ a : Bool } ∧ { b = 0 }" ["You can only combine a record with another record", "∧", "↳ { a : Bool }", "which is not a record"] + hasTypeErrorWithMessage "{ a : Bool } ∧ 0" ["You can only combine two records or two record types", "↳ { a : Bool }", "↳ 0", "↳ Natural", "↳ Type", "At least one of these arguments is neither a record type nor a record."] + hasTypeErrorWithMessage "{ a = 0 } ∧ 0" ["You can only combine a record with another record", "∧", "↳ 0", "↳ Natural", "which is not a record"] + hasTypeErrorWithMessage "0 ∧ { a : Bool }" ["You can only combine two records or two record types", "↳ { a : Bool }", "↳ 0", "↳ Natural", "↳ Type", "At least one of these arguments is neither a record type nor a record."] + hasTypeErrorWithMessage "0 ∧ { a = 0 }" ["You can only combine a record with another record", "∧", "↳ 0", "↳ Natural", "which is not a record"] + hasTypeErrorWithMessage "0 ∧ 0" ["You can only combine two records or two record types", "↳ 0", "↳ Natural", "At least one of these arguments is neither a record type nor a record."] + hasTypeErrorWithMessage "{ a : Bool } ⩓ { a : Natural }" ["Field type collision on: a", "{ x : A } ⩓ { y : B }"] + hasTypeErrorWithMessage "{ a = { b : Bool }, a = { c = 0 } }" ["Invalid duplicate field: a", "↳ { b : Bool }", "↳ Type", "which is not a record type"] + hasTypeErrorWithMessage "{ a = { b : Bool }, a = { b : Text } }" ["Field type collision on: b", "↳ b", "{ x : A } ∧ { y : B }"] + hasTypeErrorWithMessage "{ a : Bool } ⩓ { a : Natural }" ["Field type collision on: a", "↳ a", "{ x : A } ⩓ { y : B }"] + hasTypeErrorWithMessage "{ a : Bool } ⩓ { a = 0 }" ["requires arguments that are record types", "⩓", "↳ { a = 0 }", "not a record type literal"] + ) From 9557e576b95dc777600553b9889d74743da593a3 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Sat, 21 Jun 2025 14:58:52 +0200 Subject: [PATCH 26/26] better error messages and more unit tests --- dhall/src/Dhall/TypeCheck.hs | 29 +++++++++++++++++----------- dhall/tests/Dhall/Test/Regression.hs | 4 +++- 2 files changed, 21 insertions(+), 12 deletions(-) diff --git a/dhall/src/Dhall/TypeCheck.hs b/dhall/src/Dhall/TypeCheck.hs index f49c67eb5..11a5985cd 100644 --- a/dhall/src/Dhall/TypeCheck.hs +++ b/dhall/src/Dhall/TypeCheck.hs @@ -2953,9 +2953,10 @@ prettyTypeMessage (InvalidDuplicateField k expr0 expr1) = hints = [] - long = + long = -- This error occurs only when applying '∧' to two arguments, one of which is a record but the other is not. + -- Note that duplicate fields are not allowed in record types: { a : x, a : y } is never valid even if x, y are record types. "Explanation: You can specify a field twice if both fields are themselves \n\ - \records, like this: \n\ + \records or record types, like this: \n\ \ \n\ \ \n\ \ ┌──────────────────────────────────────────────────────────┐ \n\ @@ -2980,8 +2981,8 @@ prettyTypeMessage (InvalidDuplicateField k expr0 expr1) = \ └────────────────────────────────────────────────┘ \n\ \ \n\ \ \n\ - \However, this implies that both fields must be records or record types since the\n\ - \ ❰∧❱ operator cannot merge other values. Examples of invalid expressions are: \n\ + \However, this implies that both fields must be records (or both record types) as\n\ + \ the ❰∧❱ operator cannot merge other values. Examples of invalid expressions: \n\ \ \n\ \ \n\ \ ┌──────────────────┐ \n\ @@ -2994,13 +2995,18 @@ prettyTypeMessage (InvalidDuplicateField k expr0 expr1) = \ └──────────────────────────┘ \n\ \ \n\ \ \n\ + \ ┌────────────────────────────────────────┐ \n\ + \ │ { x = { a : Natural }, x = { a = 0 } } │ Invalid: The first ❰x❱ field is \n\ + \ └────────────────────────────────────────┘ a record type while the second \n\ + \ ❰x❱ field is a record \n\ + \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ \ \n\ \You specified more than one field named: \n\ \ \n\ \" <> txt0 <> "\n\ \ \n\ - \... but one of the fields had this value: \n\ + \... and one of the fields is a record but the other is not as it has this value:\n\ \ \n\ \" <> txt1 <> "\n\ \ \n\ @@ -3037,7 +3043,7 @@ prettyTypeMessage (CombineTypesRequiresRecordType expr0 expr1) = \ \n\ \ ┌───────────────────────────────────┐ \n\ \ │ λ(t : Type) → t ⩓ { name : Text } │ Invalid: ❰t❱ might not be a record \n\ - \ └───────────────────────────────────┘ type \n\ + \ └───────────────────────────────────┘ type (we only know it is a Type) \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ @@ -3264,15 +3270,16 @@ prettyTypeMessage (FieldTypeCollision c ks) = ErrorMessages {..} \ \n\ \ ┌────────────────────────────────┐ \n\ \ │ { x : Natural } " <> op <> " { x : Bool } │ Invalid: The ❰x❱ fields \"collide\" \n\ - \ └────────────────────────────────┘ because they cannot be merged \n\ - \ \n\ + \ └────────────────────────────────┘ because they cannot be merged: Natural \n\ + \ and Bool are not record types \n\ \ \n\ \... but the following expression is valid: \n\ \ \n\ \ \n\ - \ ┌────────────────────────────────────────────────┐ Valid: The ❰x❱ field \n\ - \ │ { x : { y : Bool } } " <> op <> " { x : { z : Natural } } │ types don't collide and \n\ - \ └────────────────────────────────────────────────┘ can be merged \n\ + \ ┌────────────────────────────────────────────────┐ Valid: The ❰x❱ field \n\ + \ │ { x : { y : Bool } } " <> op <> " { x : { z : Natural } } │ types are record types \n\ + \ └────────────────────────────────────────────────┘ that don't collide and \n\ + \ can be merged \n\ \ \n\ \ \n\ \────────────────────────────────────────────────────────────────────────────────\n\ diff --git a/dhall/tests/Dhall/Test/Regression.hs b/dhall/tests/Dhall/Test/Regression.hs index 176c9fd5d..3489e2d29 100644 --- a/dhall/tests/Dhall/Test/Regression.hs +++ b/dhall/tests/Dhall/Test/Regression.hs @@ -361,7 +361,7 @@ hasTypeErrorWithMessage dhallCode expectedErrorMessageSubstrings = do -- Verify that each of the expressions fails to type-check and produces a diagnostic text that contains each of the given substrings. combineTypes :: TestTree -combineTypes = Test.Tasty.HUnit.testCase "Combine / Combine Types error messages" (do +combineTypes = Test.Tasty.HUnit.testCase "Combine / CombineTypes error messages" (do hasTypeErrorWithMessage "{ a : Bool } ∧ { b = 0 }" ["You can only combine a record with another record", "∧", "↳ { a : Bool }", "which is not a record"] hasTypeErrorWithMessage "{ a : Bool } ∧ { a : Natural }" ["Field type collision on: a", "{ x : A } ∧ { y : B }"] hasTypeErrorWithMessage "{ a = 0 } ∧ { b : Natural }" ["You can only combine a record with another record", "∧", "↳ { b : Natural }", "which is not a record"] @@ -375,6 +375,8 @@ combineTypes = Test.Tasty.HUnit.testCase "Combine / Combine Types error messages hasTypeErrorWithMessage "0 ∧ 0" ["You can only combine two records or two record types", "↳ 0", "↳ Natural", "At least one of these arguments is neither a record type nor a record."] hasTypeErrorWithMessage "{ a : Bool } ⩓ { a : Natural }" ["Field type collision on: a", "{ x : A } ⩓ { y : B }"] hasTypeErrorWithMessage "{ a = { b : Bool }, a = { c = 0 } }" ["Invalid duplicate field: a", "↳ { b : Bool }", "↳ Type", "which is not a record type"] + hasTypeErrorWithMessage "{ a = { c = 0 }, a = { b : Bool } }" ["Invalid duplicate field: a", "↳ { b : Bool }", "↳ Type", "which is not a record type"] + hasTypeErrorWithMessage "{ a = { b = 0 }, a = { b = 1 } }" ["Duplicate field cannot be merged: a.b", "which collided on the following path:", "↳ a.b"] hasTypeErrorWithMessage "{ a = { b : Bool }, a = { b : Text } }" ["Field type collision on: b", "↳ b", "{ x : A } ∧ { y : B }"] hasTypeErrorWithMessage "{ a : Bool } ⩓ { a : Natural }" ["Field type collision on: a", "↳ a", "{ x : A } ⩓ { y : B }"] hasTypeErrorWithMessage "{ a : Bool } ⩓ { a = 0 }" ["requires arguments that are record types", "⩓", "↳ { a = 0 }", "not a record type literal"]