2 Notes on the new type constraint solver
3 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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)
9 See test gadt-escape1, gadt13, gadt7
10 These tests pass because of approximateImplications
12 * Equality superclasses are not getting the right instance decl
13 indexed-types/should_compile/T2238:
15 * Partial applications of data type families
16 indexed-types/should_compile/DerivingNewType
18 Functional dependencies
19 ~~~~~~~~~~~~~~~~~~~~~~~
20 * indexed-types/Gentle
22 RelaxedPolyRec by default
23 ~~~~~~~~~~~~~~~~~~~~~~~~~
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.
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?
37 * 24/7/10: canonicalisation orients meta variables
39 see trySpontaneous: need to take care with orientation
41 * See newWantedSCWorkList: no adding superclass equalities
42 for wanteds. Seems ad hoc.
44 * Happy genericTemplate notHappyAtAll needs a signature
46 * time package needs signatures; I have put -XNoMonoLocalBinds in
47 validate-settings.mk for now
51 FD1(normal) <- DV: Failure to produce FD equality from *given* and top-level
53 FD2(normal) <- DV: Failure to produce FC equality from two *givens*
57 PolyRec(normal,hpc,optasm) <- DV: Actually works, but we have a warning
58 for -XRelaxedPolyRec deprecated flag
59 T1470(normal,optc,hpc,optasm)
61 T2494-2(normal,optc,hpc,optasm)
62 T3108(normal,hpc,optasm) <- DV: Actually works, but we have a warning for
64 T3391(normal,optc,hpc,optasm)
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)
77 tc168(normal,optc,hpc,optasm) <- DV: Actually works, don't know why its reported
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)
97 * zonking Coercions should use a function of a different name
101 New modules TcSimplify (old name, but all new code)
103 TcCanonical (defines the TcS monad too)
104 Constraints (both Wanted and Canonical)
106 Existing modules Coercion (defines operations over Coercions)
109 TypeRep (the representation of types, kinds, coercions)
111 Dead modules TcTyFuns
112 TcSimplify-old.lhs (the old TcSimplify,
113 in repo just for reference)
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
122 There is no sum type combining given and wanted constraints
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
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.
137 * An evidence variable is
139 - an implicit paramter
140 - a coercion variable
141 See newEvVar in Inst.lhs
143 * The main Tc monad carries a set of untouchables
144 The unifier ensures that they are not unified
145 See Note [Unifying untouchables]
147 * tcCheckExpr does deep-skol on expected type, and
148 then calls tcExpr with (Check ty), where ty is deeply-skolemised
152 Things to check later
154 * Monomorphism restriction puts type variables in the top level env
155 When generalising, we can't generalise over these ones (alas)
157 - Reject programs that fall under the monomorphism restriction
158 (top-level monomorphic is rare)
159 - Some hack to accept H98 programs
161 * No orientation of tv~ty constraints; we don't need it
163 Note [OpenSynTyCon app]
164 ~~~~~~~~~~~~~~~~~~~~~~~
167 type family T a :: * -> *
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.
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?)