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