Overhaul of infrastructure for profiling, coverage (HPC) and breakpoints
[ghc.git] / new_tc_notes
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