Add kind equalities to GHC.
[ghc.git] / rae.txt
1 stack:
2
3 BUGS TO POST:
4 1. perfomance bug in OptCoercion: #11195
5 2. defer-type-errors are now more eager. need to float in.  #11197
6    Test cases: Defer02, T7861 (but that's impredicative)
7 3. The irreducible hetero wanteds story: #11198
8   - suboptimal error messages:
9     T9196
10     T8262
11     T8603
12     tcfail122
13
14 4. Performance: #11196
15    T3064 (14%)
16    T5030 (61.8%)
17    T5837 (13%)
18    T5321Fun (11%)
19    T5631 (39%)
20    T9872d (-91.8%)
21    T9872a (33.6%)
22    T9872c (59.4%)
23    T9872b (49.4%)
24    T9675 (29.7%) (and 28.4% peak_megabytes_allocated)
25    haddock.base (12.4%)
26    haddock.Cabal (9.5%)
27
28
29 PERFORMANCE STUFF:
30  T5030: I think the root of the problem is that I have a lot more coercions than
31  the baseline. And, I think, the reason for that is that I have a
32  (sym (a;b;c;...;zz)) where HEAD has it the right way round. During optimization,
33  the sym is pushed into the trans, and the individual pieces are axioms, which
34  resist the sym. So I get a *lot* of syms! Moving on.
35
36  T3738: I have no clue. The core appears to be the same. Is the problem
37  further down the pipeline? Ditto T5536.
38  
39  T10370: 
40
41  
42
43
44 - BUG: match_ty needs to be more delicate looking under TyConApps:
45   match_ty (Just (x :: Age)) (Just 5 |> Maybe Int ~ Maybe Age) won't work
46
47 - flattening foralls is inadequate (though not quite wrong). The tyvar
48   kind isn't flattened. Also see go_bndr in flatten_co.
49
50 fix toHsType w.r.t. implicit parameters (typecheck/should_compile/T8565.hs)
51
52 FAILURES:
53 typecheck/should_compile/T6018:
54   - TF injectivity solver fails here. The problem is that we end up with s0 ~ s1 and s0 ~ s2 in the inert
55     set, where we want to find s1 ~ s2. And, because we process deriveds last, the model doesn't get updated
56     accordingly until the end, and then there isn't the right kick-out to re-process TF injectivity stuff.
57     I would like Simon's advice.
58
59
60
61 TICKETS:
62 #9017:
63 #9173: mention expression in error
64 #7961: main ticket.
65 #10524: Typeable k
66 #8566: about dropping Given kind equalities
67 #11142: skolem escape
68
69 QUESTIONS:
70 - Should TYPE / Levity / Lifted / Unlifted be in the Prelude? If not,
71 how to deal with :info, which suppresses output that mentions un-imported things.
72 Current sol'n: make these things BuiltInSyntax.
73
74 - think about induction recursion
75 - TH will need some updating -- in particular, its treatment of quantification
76   over kinds (quantification forbidden) and types (quantification required)
77   is problematic.
78
79 - Writing a bogus GADT return type causes a panic. The problem is that
80 checkValidDataCon is supposed to check if rejigConRes was valid. To do
81 this, checkValidDataCon needs the user-specified result type. Normally,
82 this is retrieved from dataConOrigResTy. The problem is that, now,
83 the dataConOrigResTy is substed by the kind substitution produced in
84 rejigConRes. This is an ugly circular dependency. We could (1) store the
85 original, unsubsted result ty in the DataCon for just this reason, or
86 (2) install lots of ugly plumbing in TcTyClsDecls to carry the unsubsted
87 result ty, or (3) do something else. I want SPJ's input, as both (1)
88 and (2) are terrible.
89
90 - I'm deeply disturbed by match_co. It's looking into coercions! Can we fix?
91
92 fix:
93   - Make better use of TcTyCon. It could be used to remove AThing, for example.
94     Also: zonking a type could replace a TcTyCon with the same-named TyCon from
95     the monad. We'd still need a knot, but the knot would only have to surround
96     the final zonks, *not* constraint generation/solving. Vast improvement.
97
98   - DsMeta:mk_extra_tvs needs an overhaul.
99
100   - zonk_eq_types could do better with synonym expansion and injectivity tracking
101
102   - We should deprecate some old kind behavior. Specifically, consider
103     foo :: forall a. (a :: k) -> *
104     vs
105     bar :: forall a. a -> b
106
107     The first works, while the second doesn't. That's a bit inconsistent.
108
109   - better use of new VarSet features (CoreFVs using accumulators, FloatIn not converting from det
110     maps to nondet maps)
111
112   - Parser improvement ideas:
113      1. Have HsAppsTy contain alternating non-symbolic regions and symbols.
114      2. Change the _no_ops versions only to exclude dataconops, allowing * to appear.
115
116   - Refactor noThing
117
118   - Change OccurrenceOf to take a list of instantiating types. Perhaps
119     easier after visible types.
120
121   - break out NthCo into ForAllKindCo
122   - change optCoercion to take a Role hint (or perhaps a Maybe Role)
123
124   - implement better dependency checking
125
126   - Fix #15 by refusing to have kind family applications inferred in type
127     patterns.
128
129   - unifyWantedLikeEv handles coercions. But make sure other, similar scenarios
130     do too.
131
132   - Make sure coercions in types get optimised, too.
133
134   - look for uses of eqType. The typechecker should really stick to tcEqType!
135     BUT: consider making Constraint ~R *. Then, tcEqType & eqType are the same.
136   - when -fprint-explicit-coercions is on, make sure to print any types
137     of printed coboxes.
138   - make use of uo_thing in more error messages
139   - write optType. Use it instead of substTy in OptCoercion and other places.
140   - check out typecheck/should_compile/tc167.hs. It might be possible to
141     do better here. (About weird typing rule for (->))
142   - do we need to annotate kind variables to have a proper CUSK? I think so.
143     Here is Doel's example from Hac Phi of this problem at the term level:
144
145        type family Wat (t :: k) :: *
146        type instance Wat (t :: *) = Int
147        type instance Wat (t :: * -> *) = Double
148
149        data T (t :: k) = forall (t' :: k). T (Proxy t') (Wat t')
150
151        -- foo :: forall f. T f
152        foo = T (Proxy :: Proxy Maybe) 1.0
153
154
155        type family Wat (k :: *) (t :: k) :: *
156        type instance Wat *        t = Int
157        type instance Wat (* -> *) t = Double
158
159        data T (k :: *) (t :: k) :: * where
160          T :: forall (k :: *) (t :: k).
161               forall (t' :: k).
162               Proxy k t' -> Wat k t' -> T k t
163
164        foo = T (* -> *) (Any (* -> *)) Maybe Proxy 1.0
165        ???
166
167
168   - mkExpectedActualMsg has a lot of backward-compatibility stuff
169 - Are there uses of the `OrCoVar` functions that could be streamlined?
170   Also, look at uses of isCoercionType in module Id
171   - consider re-engineering the boxity problems in solver. look for the "LikeEv" functions
172
173   - Do we need special rule for boxity of ($)? I don't think so, anymore. SPJ agrees. Maybe.
174   - hsq_implict --> hsq_undeclared; hsq_explicit --> hsq_declared
175   - APromotionErr (?)
176   - :kind in GHCi is unhappy with
177     data Sg (s :: *) (t :: TyFun s * -> *) :: * where
178       (:&) :: Pi (fst :: s) -> t @@ fst -> Sg s t
179
180   - the kind-var finder in zonkRule only looks in tyvars. look in covars? how
181     to identify type-level covars? does this matter?
182   - add VisibilityFlag to Anon... see if we can sort out some constraint/* nonsense. Also, add relevance info to Anon, and work Binders into Lam and Case. This also allows us to get rid of DFunTy in iface/* stuff.
183   - perhaps change promoteCoercion --> promoteCoercion_maybe that fails if
184     it can't do any optimization.
185
186 check out usages of:
187
188 changed functions:
189
190 removed functions:
191
192 please remove:
193 --------------------------------
194 - See https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#User-facingdesignissues about constrained family instances.
195
196 - znokCtEvidence now does more zonking, because I needed that in simplifyInfer.
197
198 - dataConWrappers now are rejigged w.r.t. GADTs. This is just simpler and
199   has no user effect.
200
201 - Some interesting stuff is in TcHsType.splitTelescopeTvs, in particular see
202 Note [Typechecking telescopes].
203
204 - We are now instantiating tycons at application sites, not var sites. Very
205 interesting from a theoretical standpoint.
206
207 - There is a general assumption that all types are implicit in terms. This will have
208   to be revisited. In particular, all usages of the splitForAllTys functions will
209   need to be re-checked. Also, I think the following functions will need to be changed:
210    - mkLams
211    - tcInstType
212    - tcSplitDFunTy
213    - toIfaceClassOp
214
215 - Why isn't CPush implemented near Simplify.lhs:1200?
216
217 - Poly-kinded typeable goes to lengths to ensure that only *kind* variables
218   are around. This seems unnecessary. I've removed the code. Let's see if
219   anything breaks -- it should break rather obviously.
220
221 - (Removed) Note [Do not create Given kind equalities] says
222   "But the Right Thing is to add kind equalities!"
223
224 - *ALL* types are now kinds (of course). Including things like Double and IO.
225
226 - No kind unification algorithm (separate from that for types)
227
228 - No two coercions of the same type are ever apart.
229
230 - Promoted covar arguments in promoted datacons have role P.
231
232 - flattening a coercion flattens the types it coerces.
233
234 (old):
235 After compiling:
236 - consider adding full definition of lifting to core-spec.
237 - use optType throughout code
238 - make CoVar constructor of Var
239 - merge tcView and coreView??
240
241
242 Notes:
243
244 ----------------------------------------
245 Stuff for implementing Π:
246
247 RAE is taking a break.
248   - deeplySkolemise and its one use in tcGen have different types. Sort this out.
249   - deeplyInstantiate needs to be just like deeplySkolemise, but different.
250   - Phase information flows *up*, never *down*. That is, we always infer
251     phase information and then check when necessary. We don't try to check
252     phases top-down. This avoids the need for dependence meta-variables.
253   - How to deal with unifying Ids? This will be a problem in deeplyInstantiate.
254   - We'll need a new EvTerm (and possibly a new HsWrapper) which stores a tyvar
255     to be demoted.
256
257 stack:
258      - iface stuff
259        - ForAllTy --> PiTy
260        - ForAllCo --> PiCo
261        - function coercions are now PiCo
262        - changes in PiCoBndr
263      - matchExpectedFunTys now returns DependenceFlags
264        - unifyOpFunTysWrap returns TcPhaseType
265        - tcMatchesCase takes TcArgType
266        - tcArg takes TcArgType
267        - tcArgs does too
268        - matchFunTys callback does
269        - tcSplitSigmaTy is strange: it separates dependent things from non-dependent ones in a weird way. Remove?
270        - newSysLocalIds --> newSysLocals
271      - liftCoSubstVarBndr --> liftCoSubstBinder
272      - fix Coercion.applyCo, which shouldn't be necessary
273      - coBndrBoundVars --> coBndrBinders
274      - normalise_tycovar_bndr --> normalise_binder
275      - coreFlattenVarBndr --> coreFlattenBinder
276      - optTyVarBndr --> optBinder
277      - substTyVarBndr[Callback] -->(?) substBinder[Callback]
278      - substTyCoVarBndr2 --> substBinder2
279      - ppr_forall_type --> ppr_pi_type
280      - tidyTyCoVarBndr --> tidyBinder
281      - mkForAllTy[s] --> mkPiTy[s]
282      - removed mkNamedForAllTy
283      - mkCoercionBinder now takes a BinderVar, not a CoVar
284      - splitForAllTys --> splitPiTys
285      - splitForAllTys[B] --> splitDepPiTys
286      - tcSplitNamedForAllTysB --> tcSplitDepPiTys
287      - isForAllTy --> isPiTy, and check usages
288      - isNamedForAllTy --> isDepPiTy
289      - splitForAllTy --> splitPiTy
290      - check usages of dropForAlls: it keeps dependent products!
291      - splitForAllTysInvisible --> splitPiTysInvis; now returns Binders
292      - write cmpBinderInfo
293      - use rnBinder2 instead of rnBinderVar2
294      - nonDependentType_maybe --> nonDependentBinder_maybe
295      - prefer nonDependentType_maybe over not (isDependentBinder
296      - paDictArgType should take a Binder
297      - abstractType takes Binders
298   - fixed Named/Anon
299   - write splitPiTy_maybe
300   - write promoteExpr_maybe
301   - TyVarTy can now contain Ids!
302   - Lam takes a Binder
303   - pattern arguments are Binders
304   - fix TyCoRep.pprForAll: very broken right now. Also, see Outputable BinderVar.
305
306
307   - will need to modify FloatIn.fiExpr#mk_arg_fvs to use splitPiType instead of
308     splitFunTy
309   - will need to update DmdAnal.addDataConPatDmds to deal with strictness on
310     dependent ids
311
312
313 BEFORE MERGING:
314 Restore:
315   - README.md
316   - .gitmodules
317
318 Remove:
319   - rae.txt