1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
parser:
./a%20b
./"a%20b"
text interpolation and escapes
remove `double`
remove imports/parenthesizeUsing
remove multilet
success/
imports/
Missing missing
Headers https://example.com/foo using ./headers
HeadersInteriorHash https://example.com/foo using (./headers sha256:0000000000000000000000000000000000000000000000000000000000000000)
HeadersExteriorHash (https://example.com/foo using ./headers) sha256:0000000000000000000000000000000000000000000000000000000000000000
HeadersHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000
HeadersDoubleHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000 sha256:1111111111111111111111111111111111111111111111111111111111111111
DoubleLitPositive 1.23
DoubleLitNegative -1.23
DoubleLitExponent 1.23e4
DoubleLitExponentNoDot 1e4
DoubleLitExponentNegative 1.23e-4
DoubleLitInfinity Infinity
DoubleLitNegInfinity -Infinity
DoubleLitNaN NaN
DoubleLitSecretelyInt 1.0
DoubleLitZero 0.0
BuiltinListBuild List/Build
FunctionApplicationOneArg f x
FunctionApplicationMultipleArgs f x y z
Annotation x : T
ListLitNonEmpty [x, y]
ListLitNonEmptyAnnotated [x, y] : List T
OptionalLitEmpty []: Optional T
OptionalLitNonEmpty [x]: Optional T
Field r.x
FieldBuiltinName r.List
FieldQuoted r.`x`
Projection r.{x, y, z}
Let let x: T = v in e
LetNested let x: T = v in let y: U = w in e
LetMulti let x: T = v let y: U = w in e
LambdaUnicode λ(x : T) -> y
FunctionTypePi forall(x: T) -> U
FunctionTypePiUnicode ∀(x: T) -> U
FunctionTypePiNested forall(x: T) -> ∀(y: U) -> V
FunctionTypePiUnderscore forall(_: T) -> U
FunctionTypeArrow T -> U
RecordLit { x = 1, y = 2 }
RecordType { x: T, y: U }
operators/
ImportAlt x ? y
ImportAltAssoc w ? x ? y ? z
BoolOr x || y
BoolOrAssoc w || x || y || z
NaturalPlus x + y
NaturalPlusAssoc w + x + y + z
TextAppend x ++ y
TextAppendAssoc w ++ x ++ y ++ z
ListAppend x # y
ListAppendAssoc w # x # y # z
BoolAnd x && y
BoolAndAssoc w && x && y && z
NaturalTimes x * y
NaturalTimesAssoc w * x * y * z
BoolEQ x == y
BoolEQAssoc w == x == y == z
BoolNE x != y
BoolNEAssoc w != x != y != z
RecursiveRecordMerge x //\\ y
RecursiveRecordMergeAssoc w //\\ x //\\ y //\\ z
RecursiveRecordTypeMerge x /\ y
RecursiveRecordTypeMergeAssoc w /\ x /\ y /\ z
RightBiasedRecordMerge x // y
RightBiasedRecordMergeAssoc w // x // y // z
RecursiveRecordMergeUnicode x ∧ y
RecursiveRecordMergeUnicodeAssoc w ∧ x /\ y ∧ z
RightBiasedRecordMergeUnicode x ⫽ y
RightBiasedRecordMergeUnicodeAssoc w ⫽ x // y ⫽ z
RecursiveRecordTypeMergeUnicode x ⩓ y
RecursiveRecordTypeMergeUnicodeAssoc w ⩓ x //\\ y ⩓ z
PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o
PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n
PrecedenceNat a + b * d + e f * (g + h)
PrecedenceBool a && b || c d == e || f != g && h || i
PrecedenceRecord a // b c /\ d ⫽ e.{x} ∧ f
failure/
ProjectionByExpressionNeedsParens r.{ x: T }
import:
success/
recover type error
recover recursive import error
failure/
don't recover cycle
normalization:
variables across import boundaries
TextLitNested1 "${""}${x}"
TextLitNested2 "${"${x}"}"
TextLitNested3 "${"${""}"}${x}"
EquivalenceDouble if b then NaN else NaN
EquivalenceAlpha if b then \(x: T) -> x else \(y: T) -> y
typecheck:
something that involves destructuring a recordtype after merge
success/
MergeEmptyAlternative merge { x = 1 } < x >.x
MergeTrickyShadowing let _ = Bool in merge {_ = \(x: _) -> x} (<_: Bool>._ True)
EquivalenceAlpha \(TODO: forall(x: Type) -> x) -> TODO : forall(y: Type) -> y
failure/
MergeEmptyNeedsDirectAnnotation1 \(x: <>) -> (merge {=} x) : Bool
MergeEmptyNeedsDirectAnnotation2 \(x: <>) -> let y: Bool = merge {=} x in 1
MergeBoolIsNotUnion merge x True
MergeOptionalIsNotUnion merge x (Some 1)
MergeMissingHandler1 merge {=} < x >.x
MergeMissingHandler2 merge {x=...,} <x|y>.x
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x
merge {x=...,y=...} <x>.x
merge {x=...,y=...} <x:T>.x
MergeHandlerFreeVar merge { x = None } < x = Bool >
UnionTypeDuplicateVariants1 <x, x>
UnionTypeDuplicateVariants2 <x, x:T>
UnionLitDuplicateVariants <x=1|x:T>
RecordLitDuplicateFields { x: T, x: T }
EquivalenceAlphaTrap \(TODO: forall(_: Type) -> _) -> TODO : forall(x: Type) -> _
equivalence:
|
