summaryrefslogtreecommitdiff
path: root/new_tc_notes
blob: bf75f9b3ac206cd4ac4776811ed0f445e8a12492 (plain)
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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181

Notes on the new type constraint solver
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* 1/9/10: Consider
    {alpha} [b] (c~b) => (alpha ~ b)
  Then to maximise the chance of floating the equality out of
  the implication we'd like to orient the given as (b~c) 
  rather than (c~b).
     See test gadt-escape1, gadt13, gadt7
  These tests pass because of approximateImplications

* Equality superclasses are not getting the right instance decl
    indexed-types/should_compile/T2238:

* Partial applications of data type families
    indexed-types/should_compile/DerivingNewType
  
Functional dependencies
~~~~~~~~~~~~~~~~~~~~~~~
* indexed-types/Gentle

RelaxedPolyRec by default
~~~~~~~~~~~~~~~~~~~~~~~~~
* tcfail071
* tcfail144
* tcfail149, 150


---------------------
* 18/8/10: Fixed treatment of new work list from superclasses of wanteds. 
           TODO TODO: Revisit the desugarer to deal with equalities that 
           may mention recursive dictionaries. 

* 12/8/10: Fixed proper kind checking for equalities and type family equalities.
  NOTE: Type synonyms stay unexpanded in canonical constraints. Is this correct?

* 24/7/10: canonicalisation orients meta variables
           kind checking?
  see trySpontaneous: need to take care with orientation 

* See newWantedSCWorkList: no adding superclass equalities
  for wanteds.  Seems ad hoc.

* Happy genericTemplate notHappyAtAll needs a signature

* time package needs signatures; I have put -XNoMonoLocalBinds in 
     validate-settings.mk for now

Improve error message
~~~~~~~~~~~~~~~~~~~~~
   FD1(normal)          <- DV: Failure to produce FD equality from *given* and top-level

   FD2(normal)          <- DV: Failure to produce FC equality from two *givens*

Unexpected failures:
~~~~~~~~~~~~~~~~~~~~~
   PolyRec(normal,hpc,optasm)     <- DV: Actually works, but we have a warning 
                                     for -XRelaxedPolyRec deprecated flag
   T1470(normal,optc,hpc,optasm)   
   T2494(normal)
   T2494-2(normal,optc,hpc,optasm)
   T3108(normal,hpc,optasm)       <- DV: Actually works, but we have a warning for 
                                     deprecated flags
   T3391(normal,optc,hpc,optasm)  
   tc003(hpc)
   tc081(normal,optc,hpc,optasm)  <- DV: Let does not get generalized for 
                                         *single* variable binding
   tc089(normal,optc,hpc,optasm)       
   tc095(normal,optc,hpc,optasm)
   tc111(normal,optc,hpc,optasm)
   tc113(normal,optc,hpc,optasm)  Generalize top-level var binding
   tc127(normal,optc,hpc,optasm)  <- DV: Missing module Maybe in haskell98 package ... 
   tc132(normal,optc,hpc,optasm)  Generalize top-level var binding
   tc150(normal,optc,hpc,optasm)  Pattern signatures 
   tc159(normal,optc,hpc,optasm)  <- ILL FORMED EVIDENCE (related to newtype ... deriving) 
   tc162(normal)
   tc168(normal,optc,hpc,optasm)  <- DV: Actually works, don't know why its reported
   tc170(normal)
   tc175(normal,optc,hpc,optasm)
   tc189(normal,optc,hpc,optasm)  <- higher-rank ? 
   tc192(normal,optc,hpc,optasm)  <- loop in desugarer
   tc194(normal,optc,hpc,optasm)  <- polymorphic pattern signatures / higher-rank?
   tc211(normal,optc,hpc,optasm)  <- polymorphic pattern signatures / higher-rank?
   tc216(normal,optc,hpc,optasm)  <- ctx stack depth exceeded ... 
   tc217(normal,optc,hpc,optasm)  
   tc222(normal,optc,hpc,optasm)
   tc231(normal,optc,hpc,optasm)
   tc237(normal,optc,hpc,optasm)
   tc243(normal,optc,hpc,optasm)      <- DV: Actually works, Definition but no signature warning 
   tc244(normal,optc,hpc,optasm)


 

ToDo
~~~~
* zonking Coercions should use a function of a different name

Basic setup
~~~~~~~~~~~
   New modules     TcSimplify (old name, but all new code)
		   TcInteract
                   TcCanonical (defines the TcS monad too)
                   Constraints (both Wanted and Canonical)

Existing modules   Coercion (defines operations over Coercions)
	 	   Kind
	 	   Type
		   TypeRep (the representation of types, kinds, coercions)

   Dead modules	   TcTyFuns
		   TcSimplify-old.lhs (the old TcSimplify, 
			in repo just for reference)


Significant differences wrt the prototype
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* "Givens"  are simply evidence variables (EvVar)
  "Wanteds" are WantedConstraints
  See the Implication type in TcSolverTypes.lhs

  There is no sum type combining given and wanted constraints

* Wanted constraints are of three flavours (see data WantedConstraint)
	- evidenence variables: we can abstract over these
	- implications: we can't abstract over these
        - literal and method constraints; we can't abstract over these
		either, and they aren't implemented yet

* We use a mutable group of bindings attached to each Inplication as the
  place to accumulate evidence for dictionaries and implicit parameters
  (It's also vital for equality superclasses.)  Each Impliciation has a
  TcEvBinds, defined in hsSyn/HsBinds.  The reference cell to accumulate
  bindings into is carried by the TcS solver monad; we need to fill in 
  evidence in the solver.

* An evidence variable is
	- a dictionary
	- an implicit paramter
	- a coercion variable
  See newEvVar in Inst.lhs

* The main Tc monad carries a set of untouchables
  The unifier ensures that they are not unified
  See Note [Unifying untouchables]

* tcCheckExpr does deep-skol on expected type, and
  then calls tcExpr with (Check ty), where ty is deeply-skolemised


-------------------
Things to check later
-------------------
* Monomorphism restriction puts type variables in the top level env
  When generalising, we can't generalise over these ones (alas)
  Consider: 
    - Reject programs that fall under the monomorphism restriction
        (top-level monomorphic is rare)
    - Some hack to accept H98 programs

* No orientation of tv~ty constraints; we don't need it

Note [OpenSynTyCon app]
~~~~~~~~~~~~~~~~~~~~~~~
Given

  type family T a :: * -> *

the two types (T () a) and (T () Int) must unify, even if there are
no type instances for T at all.  Should we just turn them into an
equality (T () a ~ T () Int)?  I don't think so.  We currently try to
eagerly unify everything we can before generating equalities; otherwise,
we could turn the unification of [Int] with [a] into an equality, too.

------------------------
We need to both 'unBox' and zonk deferred types.  We need to unBox as
functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected
type.  We need to zonk as the types go into the kind of the coercion variable
`cotv' and those are not zonked in Inst.zonkInst.  (Maybe it would be better
to zonk in zonInst instead.  Would that be sufficient?)