[GHC] #12918: Make DefaultSignatures more particular about their types on the RHS of a context

[GHC]

#12918: Make DefaultSignatures more particular about their types on the RHS of a
context
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  simonpj
            Type:  bug               |               Status:  patch
        Priority:  normal            |            Milestone:  8.2.1
       Component:  Compiler (Type    |              Version:  8.0.2-rc1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #12784            |  Differential Rev(s):  Phab:D2983
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Consider
 {{{
 class C a b where
   op         :: forall p q. (Ord a, D p q) => a -> b -> (a,b)
   default op :: forall r. (E r)            => a -> b -> (a,b)
 }}}
 We are expecting the part after the `=>` to be identical.

 In `check_dm` in `checkValidClass` we have in hand:

 * `sel_id :: forall aa bb. C aa bb => forall p q. (Ord p, D p q) => aa ->
 bb -> p -> (aa,bb)`.
   Note that `sel_id` always has this form: see `sel_ty` in
 `MkId.mkDictSelId`

 * Inside class `C a b` we have a `GemericDM (forall r s. (E r) => a -> b
 -> s -> (a,b)`.  This is passed to `check_dm`.

 Notice that, as commented with `Class.DefMethInfo`, the `ty` in
 `(GenericDM ty)` is ''not'' quantified over the class variables `a` and
 `b`.

 But `sel_id` ''is'' so quantified, and in principle its foralls, here `aa`
 and `bb`, might be different to the class tyvars `a` and `b`.  (This will
 never happen in practice, but still.)

 What we want is to match up these two types
 {{{
 From sel_id:      C aa bb => aa -> bb -> p -> (aa,bb)
 From GenericDM:   C a  b  => a  -> b  -> s -> (a, b)
 }}}
 This is a '''one-way match''': use `tcMatchTy`.  Not unification!

 We need the `C a b` part to match up `a` with `aa` and `b` with `bb`.

 If successful we'll emerge with a mapping `[a -> aa, b -> bb, s -> p]`.

 Is that enough?  No: we need to ensure that each variable in the domain of
 the substitution maps to a distinct type variable in the range. For
 example `[s -> Int]` would not be OK.  I think
 `TcValidity.allDistinctTyVars` is what you want.

 Does that help?

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