[GHC] #12526: regression in type inference with respect to type families

[GHC]

#12526: regression in type inference with respect to type families
-------------------------------------+-------------------------------------
        Reporter:  Lemming           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.2
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  10634             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I spent some time finding out what is going on here.

 * We typecheck the binding for `osci` with generalisation (despite
 `NoMonoBinds`) because the RHS has no locally-bound free variables.

 * But `osci` triggers the monomorphism restriction because of the `(CP t)`
 constraint.

 * So from `osci`s binding we initially get (where `pp` is a unification
 variable)
 {{{
 osci :: pp Float Float
 Constraints: CP pp
 }}}

 * However, during inference of `osci`'s type we try to simplify those
 constraints (`simplifyInfer`).  So we get
 {{{
     [W] CP pp

 --> add derived superclass constraints

     [W] CP pp
     [D] pp ~ P (S pp)

 But we flatten those constraints to get

 --> flatten (the fuv1/2 are flatten-meta-vars)

     [W] CP pp
     [D] pp ~ fuv1
     [D] S pp   ~ fuv2    (CFunEqCan)
     [D] P fuv2 ~ fuv1    (CFunEqCan)

 --> Now (here is the problem) we unify pp := fuv1

     [W] CP fuv1
     [D] S fuv1 ~ fuv2    (CFunEqCan)
     [D] P fuv2 ~ fuv1    (CFunEqCan)

 --> Nothing further happens, so we unflatten to get

     fuv1 := P fuv2
     [W] CP (P fuv2)
     [D] P (S fuv2) ~ fuv2

 Discarding the derived constraint we have ended up with
     osci :: P fuv2 Float Float
     Constaints: CP (P fuv2)
 }}}

 * But replacinng `pp := P fuv2` is bad, because in the call `f osci`, we
 now get
 {{{
   [W] Causal Float Float ~ P fuv2 Float Float
 }}}
   which leads to `P fuv2 ~ Causal`, which doesn't tell us how to choose
 `fuv2`.  If we had only left it alone, we'd have had
 {{{
   [W] Causal Float Float ~ pp Float Float
 }}}
   which tells us `p := Causal` and everything gets solved.

 I have not investigated why it worked before, but it's clearly terribly
 delicate.  For now I'm just recording the breadcrumbs.

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