[GHC] #9318: Type error reported in wrong place with repeated type family expressions

[GHC]

#9318: Type error reported in wrong place with repeated type family expressions
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |            Owner:  simonpj
                  Type:  bug         |           Status:  new
              Priority:  high        |        Milestone:  7.10.1
             Component:  Compiler    |          Version:  7.8.3
  (Type checker)                     |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Capturing work in progress.

 I've pushed a second iteration to branch `wip/new-flatten-skolems-Aug14`.
 Still not really right.

 An interesting case is `indexed-types/should_compile/T3826`; see commments
 in the source file.

 Below are my notes
 {{{
 ToDo:

 * TcInteract, Note [Efficient orientation]?

 * inert_funeqs, inert_eqs: keep only the CtEvidence.
    They are all CFunEqCans, CTyEqCans

 * Update Note [Preparing inert set for implications]

 * indexed_types/should_compile/T3826


 The new flattening story
 ~~~~~~~~~~~~~~~~~~~~~~~~

 * A "flatten-skolem", fsk, is a *unification* variable
   (ie with an IORef inside it)

 * A CFunEqCan is always of form
      [W] x : F xis ~ fsk
   where
      x is the witness variable
      fsk is a flatten skolem
      xis are function-free
   CFunEqCans are always [Wanted], never [Given] or [Derived]

 * Inert set invariant: if [W] F xis1 ~ fsk1, [W] F xis2 ~ fsk2
                        then xis1 /= xis2
   i.e. at most one CFunEqCan with a particular LHS

 * Each canonical CFunEqCan [W] x : F xis ~ fsk has its own
   distinct evidence variable x and flatten-skolem fsk.

 * CFunEqCans are the *only* way that function applications appear in
   canonical constraints.  Function applications in any other
   constraint must be gotten rid of by flattening, thereby generating
   fresh CFunEqCans.

 * Flattening a type (F xis):
     - Make a new [W] x : F xis ~ fsk
       with fresh evidence variable x and flatten-skolem fsk

     - Add it to the work list

     - Replace (F xis) with fsk in the type you are flattening

     - You can also add the CFunEqCan to the "flat cache", which
       simply keeps track of all the function applications you
       have flattened. If (F xis) is in the cache already, just
       use its fsk and evidence x, and emit nothing.

     - No need to substitute in the flat-cache. It's not the end
       of the world if we start with, say (F alpha ~ fsk1) and
       (F Int ~ fsk2) and then find alpha := Int.  Athat will
       simply give rise to fsk1 := fsk2 via [Interacting rule] below

 * Canonicalising ([W} x : F xis ~ fsk)
     - Flatten xis cos :: xis ~ flat_xis
     - New wanted  x2 :: F flat_xis ~ fsk
     - Add new wanted to flat cache
     - Discharge x = F cos ; x2

 * Flatten-skolems ONLY get unified when either
     a) The CFunEqCan takes a step, using an axiom
     b) During un-flattening at the very, very end
   They are never unified in any other form of equality.
   For example [W] fsk ~ Int  is stuck; it does not unify with fsk.

 * We *never* substitute in the RHS (i.e. the fsk) of a CFunEqCan.
   That would destroy the invariant about the shape of a CFunEqCan,
   and it would risk wanted/wanted interactions. The only way we
   learn information about fsk is when the CFunEqCan takes a step.

   However we *do* substitute in the LHS of a CFunEqCan (else it
   would never get to fire!)

 * KEY INSIGHTS:
    - A flatten-skolem stands for the as-yet-unknown type to which
      (F xis) will eventually reduce
    - Although the CFunEqCan is a Wanted, it will almost always
      eventually be solved, eitehr

 * [Interacting rule]
     (inert)     x1 : F tys ~ fsk1
     (work item) x2 : F tys ~ fsk2
   Just solve one from the other:
     x2 := x1
     fsk2 := fsk1
     [G] <fsk1> fsk2 ~ fsk1
   This just unites the two fsks into one.

 * [Firing rule]
     (work item) x : F tys ~ fsk
     instantiate axiom: co : F tys ~ rhs

    First flatten rhs, giving
       flat_co : rhs ~ xi

    Now unify
       fsk := xi
       [G] <xi> : fsk ~ xi
       x := co ; flat_co
    discharging the work item

    UNLESS fsk appears in xi, which can happen, in which case
    don't unnify but stick [W] fsk ~ xi in the insoluble set.

 ---------------
 ----------------
 Preparing the inert set for implications

    type instance F True a b = a
    type instance F False a b = b

    [W] x : F c a b ~ fsk
    [G] gamma ~ fsk
    (c ~ True)  => a ~ gamma
    (c ~ False) => b ~ gamma
 --> (c ~ True branch)  Push in as given non-canonical
    [G] g : (c ~ True)
    [G] x : F c a b ~ fsk  (nc)
    [W] a ~ fsk,
 --> flatten
    [G] g : (c ~ True)
    [G] sym x1 ; x : fsk1 ~ fsk
    [W] x1 : F c a b ~ fsk1 (canon)
    [W] a ~ fsk,
 ---> subst c
    [G] g : (c ~ True)
    [G] sym x1 ; x : fsk1 ~ fsk
    [W] x2 : F True a b ~ fsk1 (canon)
    x1 = F g a b ; x2
    [W] a ~ fsk,
 ---> step  ax : F True a b ~ a
    [G] g : (c ~ True)
    [G] sym x1 ; x : fsk1 ~ fsk
    [W] x2 : F True a b ~ fsk1 (canon)
    [G] <a> : fsk1 := a
    x2 = ax

    [W] a ~ fsk,

 --------------------------
 Simple20
 ~~~~~~~~
  axiom F [a] = [F a]

  [G] F [a] ~ a
 -->
  [G] fsk ~ a
  [W] F [a] ~ fsk
 -->
  fsk := [fsk2]
  [G] [fsk2] ~ a
  [W] F a ~ fsk2
 -->
  [W] F [fsk2] ~ fsk2   -- Back to square 1
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9318#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler