[GHC] #13398: Associated type family instance validity checking is too conservative

[GHC]

#13398: Associated type family instance validity checking is too conservative
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.2.1
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11450            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > To better illustrate the point I'm trying to make, imagine you instead
 had this code:

 Ah. Excellent point.

 An easy thing to do is simply to lift the check altogether.  So the result
 would be

 * The args corresponding to the class parameters must be identical
 * The other args can be anything at all

 So we'd allow
 {{{
 class C a where
   type F a b
   ...

 instance C Int where
   type F Int Bool = Char
   ...
 }}}
 That says nothing about what `F Int Char` might be; and you can only give
 instances for `F` inside a class `instance`, so you can't extend it later.

 We could get this simply by omitting the two `check_poly_arg` lines in
 `TcValidity.checkConsistntFamInst`:
 {{{
        -- Check type args first (more comprehensible)
        ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
        ; checkTc (check_poly_args type_shapes) pp_wrong_at_tyvars

        -- And now kind args
        ; checkTc (all check_arg kind_shapes)
                  (pp_wrong_at_arg $$ ppSuggestExplicitKinds)
        ; checkTc (check_poly_args kind_shapes)
                  (pp_wrong_at_tyvars $$ ppSuggestExplicitKinds)
 }}}
 Alternatively I suppose we could instead elaborate the check to allow
 single-constructor data types to be pattern matched as above.  (Nestedly,
 I guess.)

 Alternatively, we could just make a refutable pattern into a warning.  But
 watch out for `type F Int r r`, which demands equality.

 I don't know which is best.  Whatever the outcome, would you like to push
 this through, Ryan?

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