You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: dhall/src/Dhall/TypeCheck.hs
+33-26Lines changed: 33 additions & 26 deletions
Original file line number
Diff line number
Diff line change
@@ -843,19 +843,24 @@ infer typer = loop
843
843
844
844
(VConst cL, VRecord xLs', VConst cR, VRecord xRs') ->do-- Both arguments are record types.
845
845
let c =max cL cR
846
-
recordTypesHaveNoFieldCollisions [] xLs' xRs'
846
+
recordTypesHaveNoFieldCollisions '∧'[] xLs' xRs'
847
847
return (VConst c)
848
848
849
-
(VRecord _, _, _, _) ->do-- The left argument is a record term, the right argument is not. The error is in the right argument.
849
+
(VRecord _, _, _, _) ->do-- The left argument is a record term, the right argument is not. We report the error in the right argument.
850
850
case mk of
851
851
Nothing-> die (MustCombineARecord'∧' r'' _R'')
852
852
Just t -> die (InvalidDuplicateField t r _R'')
853
853
854
-
(VConst _, VRecord _, _, _) ->do-- The left argument is a record type, the right argument is not. The error is in the right argument.
855
-
die (CombineTypesRequiresRecordType r r'')
854
+
(_, _, VRecord _, _) ->do-- The right argument is a record term, the left argument is not. We report the error in the left argument.
855
+
case mk of
856
+
Nothing-> die (MustCombineARecord'∧' l'' _L'')
857
+
Just t -> die (InvalidDuplicateField t l _L'')
858
+
859
+
(VConst _, VRecord _, _, _) ->do-- The left argument is a record type, the right argument is not. We report the error in the right argument.
860
+
die (MustCombineRecordsOrRecordTypes'∧' r r'')
856
861
857
-
_ ->do-- The error is in the left argument: it must be either a record term or a record type, but it is neither.
858
-
die (MustCombineARecordOrRecordType'∧' l l'')
862
+
_ ->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.
863
+
die (MustCombineRecordsOrRecordTypes'∧' l l'')
859
864
860
865
861
866
CombineTypes _ l r ->do
@@ -889,7 +894,7 @@ infer typer = loop
889
894
VRecord xRs' ->return xRs'
890
895
_ -> die (CombineTypesRequiresRecordType r r'')
891
896
892
-
recordTypesHaveNoFieldCollisions [] xLs' xRs'
897
+
recordTypesHaveNoFieldCollisions '⩓'[] xLs' xRs'
893
898
894
899
return (VConst c)
895
900
@@ -1359,13 +1364,13 @@ infer typer = loop
1359
1364
1360
1365
quote ns value =Dhall.Core.renote (Eval.quote ns value)
1361
1366
1362
-
recordTypesHaveNoFieldCollisions xs xLs₀' xRs₀' =Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR)
1367
+
recordTypesHaveNoFieldCollisions c xs xLs₀' xRs₀' =Foldable.sequence_ (Data.Map.intersectionWithKey combine mL mR)
0 commit comments