Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100644 180 lines (143 sloc) 6.672 kb
d2ce0f52 » simonpj@microsoft.com
2010-09-13 Super-monster patch implementing the new typechecker -- at last
1
2 Notes on the new type constraint solver
3 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4 * 1/9/10: Consider
5 {alpha} [b] (c~b) => (alpha ~ b)
6 Then to maximise the chance of floating the equality out of
7 the implication we'd like to orient the given as (b~c)
8 rather than (c~b).
9 See test gadt-escape1, gadt13, gadt7
10 These tests pass because of approximateImplications
11
12 * Equality superclasses are not getting the right instance decl
13 indexed-types/should_compile/T2238:
14
15 * Partial applications of data type families
16 indexed-types/should_compile/DerivingNewType
17
18 Functional dependencies
19 ~~~~~~~~~~~~~~~~~~~~~~~
20 * indexed-types/Gentle
21
22 RelaxedPolyRec by default
23 ~~~~~~~~~~~~~~~~~~~~~~~~~
24 * tcfail071
25 * tcfail144
26 * tcfail149, 150
27
28
29 ---------------------
30 * 18/8/10: Fixed treatment of new work list from superclasses of wanteds.
31 TODO TODO: Revisit the desugarer to deal with equalities that
32 may mention recursive dictionaries.
33
34 * 12/8/10: Fixed proper kind checking for equalities and type family equalities.
35 NOTE: Type synonyms stay unexpanded in canonical constraints. Is this correct?
36
37 * 24/7/10: canonicalisation orients meta variables
38 kind checking?
39 see trySpontaneous: need to take care with orientation
40
41 * See newWantedSCWorkList: no adding superclass equalities
42 for wanteds. Seems ad hoc.
43
44 * Happy genericTemplate notHappyAtAll needs a signature
45
46 * time package needs signatures; I have put -XNoMonoLocalBinds in
47 validate-settings.mk for now
48
49 Improve error message
50 ~~~~~~~~~~~~~~~~~~~~~
51 FD1(normal) <- DV: Failure to produce FD equality from *given* and top-level
52
53 FD2(normal) <- DV: Failure to produce FC equality from two *givens*
54
55 Unexpected failures:
56 ~~~~~~~~~~~~~~~~~~~~~
57 PolyRec(normal,hpc,optasm) <- DV: Actually works, but we have a warning
58 for -XRelaxedPolyRec deprecated flag
59 T1470(normal,optc,hpc,optasm)
60 T2494(normal)
61 T2494-2(normal,optc,hpc,optasm)
62 T3108(normal,hpc,optasm) <- DV: Actually works, but we have a warning for
63 deprecated flags
64 T3391(normal,optc,hpc,optasm)
65 tc003(hpc)
66 tc081(normal,optc,hpc,optasm) <- DV: Let does not get generalized for
67 *single* variable binding
68 tc089(normal,optc,hpc,optasm)
69 tc095(normal,optc,hpc,optasm)
70 tc111(normal,optc,hpc,optasm)
71 tc113(normal,optc,hpc,optasm) Generalize top-level var binding
72 tc127(normal,optc,hpc,optasm) <- DV: Missing module Maybe in haskell98 package ...
73 tc132(normal,optc,hpc,optasm) Generalize top-level var binding
74 tc150(normal,optc,hpc,optasm) Pattern signatures
75 tc159(normal,optc,hpc,optasm) <- ILL FORMED EVIDENCE (related to newtype ... deriving)
76 tc162(normal)
77 tc168(normal,optc,hpc,optasm) <- DV: Actually works, don't know why its reported
78 tc170(normal)
79 tc175(normal,optc,hpc,optasm)
80 tc189(normal,optc,hpc,optasm) <- higher-rank ?
81 tc192(normal,optc,hpc,optasm) <- loop in desugarer
82 tc194(normal,optc,hpc,optasm) <- polymorphic pattern signatures / higher-rank?
83 tc211(normal,optc,hpc,optasm) <- polymorphic pattern signatures / higher-rank?
84 tc216(normal,optc,hpc,optasm) <- ctx stack depth exceeded ...
85 tc217(normal,optc,hpc,optasm)
86 tc222(normal,optc,hpc,optasm)
87 tc231(normal,optc,hpc,optasm)
88 tc237(normal,optc,hpc,optasm)
89 tc243(normal,optc,hpc,optasm) <- DV: Actually works, Definition but no signature warning
90 tc244(normal,optc,hpc,optasm)
91
92
93
94
95 ToDo
96 ~~~~
97 * zonking Coercions should use a function of a different name
98
99 Basic setup
100 ~~~~~~~~~~~
101 New modules TcSimplify (old name, but all new code)
102 TcInteract
103 TcCanonical (defines the TcS monad too)
104 Constraints (both Wanted and Canonical)
105
106 Existing modules Coercion (defines operations over Coercions)
107 Kind
108 Type
109 TypeRep (the representation of types, kinds, coercions)
110
111 Dead modules TcTyFuns
112 TcSimplify-old.lhs (the old TcSimplify,
113 in repo just for reference)
114
115
116 Significant differences wrt the prototype
117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
118 * "Givens" are simply evidence variables (EvVar)
119 "Wanteds" are WantedConstraints
120 See the Implication type in TcSolverTypes.lhs
121
122 There is no sum type combining given and wanted constraints
123
124 * Wanted constraints are of three flavours (see data WantedConstraint)
125 - evidenence variables: we can abstract over these
126 - implications: we can't abstract over these
127 - literal and method constraints; we can't abstract over these
128 either, and they aren't implemented yet
129
130 * We use a mutable group of bindings attached to each Inplication as the
131 place to accumulate evidence for dictionaries and implicit parameters
132 (It's also vital for equality superclasses.) Each Impliciation has a
133 TcEvBinds, defined in hsSyn/HsBinds. The reference cell to accumulate
134 bindings into is carried by the TcS solver monad; we need to fill in
135 evidence in the solver.
136
137 * An evidence variable is
138 - a dictionary
139 - an implicit paramter
140 - a coercion variable
141 See newEvVar in Inst.lhs
142
143 * The main Tc monad carries a set of untouchables
144 The unifier ensures that they are not unified
145 See Note [Unifying untouchables]
146
147 * tcCheckExpr does deep-skol on expected type, and
148 then calls tcExpr with (Check ty), where ty is deeply-skolemised
149
150
151 -------------------
152 Things to check later
153 -------------------
154 * Monomorphism restriction puts type variables in the top level env
155 When generalising, we can't generalise over these ones (alas)
156 Consider:
157 - Reject programs that fall under the monomorphism restriction
158 (top-level monomorphic is rare)
159 - Some hack to accept H98 programs
160
161 * No orientation of tv~ty constraints; we don't need it
162
163 Note [OpenSynTyCon app]
164 ~~~~~~~~~~~~~~~~~~~~~~~
165 Given
166
167 type family T a :: * -> *
168
169 the two types (T () a) and (T () Int) must unify, even if there are
170 no type instances for T at all. Should we just turn them into an
171 equality (T () a ~ T () Int)? I don't think so. We currently try to
172 eagerly unify everything we can before generating equalities; otherwise,
173 we could turn the unification of [Int] with [a] into an equality, too.
174
175 ------------------------
176 We need to both 'unBox' and zonk deferred types. We need to unBox as
177 functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected
178 type. We need to zonk as the types go into the kind of the coercion variable
179 `cotv' and those are not zonked in Inst.zonkInst. (Maybe it would be better
180 to zonk in zonInst instead. Would that be sufficient?)
181
Something went wrong with that request. Please try again.