Re: [GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

5 Nov 2017

      #14331: Overzealous free-floating kind check causes deriving clause to be rejected
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  deriving
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  GHC rejects       |            Test Case:
  valid program                      |  deriving/should_compile/T14331
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I made an attempt towards fixing this at
 https://github.com/RyanGlScott/ghc/tree/rgs/T14331. I didn't get very far.

 My first goal was to switch over from the use of the pure unifier to the
 monadic one, but that alone proves to be quite difficult. The problem is
 that for some strange reason, using the monadic unifier causes several
 type variables to be filled in with `Any`, leading to Core Lint errors and
 general badness. As one example, if you compile this program:

 {{{#!hs
 module Bug where

 data Pair a b = Pair a b
   deriving Eq
 }}}

 Using my branch with `-dcore-lint` on, you'll be greeted with this:

 {{{
 $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs -dcore-lint
 GHCi, version 8.3.20171031: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 *** Core Lint errors : in result of Desugar (after optimization) ***
 Bug.hs:4:12: warning:
     [RHS of $fEqPair :: forall a b.
                         (Eq Any, Eq Any) =>
                         Eq (Pair Any Any)]
     The type of this binder doesn't match the type of its RHS: $fEqPair
     Binder's type: forall a b. (Eq Any, Eq Any) => Eq (Pair Any Any)
     Rhs type: forall a b. (Eq b, Eq a) => Eq (Pair a b)
 *** Offending Program ***
 $c==_a2Cw
   :: forall a b. (Eq b, Eq a) => Pair a b -> Pair a b -> Bool
 [LclId]
 $c==_a2Cw
   = \ (@ a_a2Cr)
       (@ b_a2Cs)
       ($dEq_a2Ct :: Eq b_a2Cs)
       ($dEq_a2Cu :: Eq a_a2Cr)
       (ds_d2Dz :: Pair a_a2Cr b_a2Cs)
       (ds_d2DA :: Pair a_a2Cr b_a2Cs) ->
       case ds_d2Dz of { Pair a1_a2Cn a2_a2Co ->
       case ds_d2DA of { Pair b1_a2Cp b2_a2Cq ->
       &&
         (== @ a_a2Cr $dEq_a2Cu a1_a2Cn b1_a2Cp)
         (== @ b_a2Cs $dEq_a2Ct a2_a2Co b2_a2Cq)
       }
       }

 Rec {
 $fEqPair [InlPrag=NOUSERINLINE CONLIKE]
   :: forall a b. (Eq Any, Eq Any) => Eq (Pair Any Any)
 [LclIdX[DFunId],
  Unf=DFun: \ (@ a_a2z3[tau:1])
              (@ b_a2z4[tau:1])
              (v_B1 :: Eq b_a2z4[tau:1])
              (v_B2 :: Eq a_a2z3[tau:1]) ->
        C:Eq TYPE: Pair a_a2z3[tau:1] b_a2z4[tau:1]
             $c==_a2Cw @ a_a2z3[tau:1] @ b_a2z4[tau:1] v_B1 v_B2
             $c/=_a2CF @ a_a2z3[tau:1] @ b_a2z4[tau:1] v_B1 v_B2]
 $fEqPair
   = \ (@ a_a2Cr)
       (@ b_a2Cs)
       ($dEq_a2Ct :: Eq b_a2Cs)
       ($dEq_a2Cu :: Eq a_a2Cr) ->
       C:Eq
         @ (Pair a_a2Cr b_a2Cs)
         ($c==_a2Cw @ a_a2Cr @ b_a2Cs $dEq_a2Ct $dEq_a2Cu)
         ($c/=_a2CF @ a_a2Cr @ b_a2Cs $dEq_a2Ct $dEq_a2Cu)

 $c/=_a2CF [Occ=LoopBreaker]
   :: forall a b. (Eq b, Eq a) => Pair a b -> Pair a b -> Bool
 [LclId]
 $c/=_a2CF
   = \ (@ a_a2Cr)
       (@ b_a2Cs)
       ($dEq_a2Ct :: Eq b_a2Cs)
       ($dEq_a2Cu :: Eq a_a2Cr) ->
       $dm/=
         @ (Pair a_a2Cr b_a2Cs)
         ($fEqPair @ a_a2Cr @ b_a2Cs $dEq_a2Ct $dEq_a2Cu)
 end Rec }

 $trModule :: Module
 [LclIdX]
 $trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)

 $krep_a2Dx [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a2Dx = $WKindRepVar (I# 1#)

 $krep_a2Dv [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a2Dv = $WKindRepVar (I# 0#)

 $tcPair :: TyCon
 [LclIdX]
 $tcPair
   = TyCon
       13156152634686180623##
       12550973000996521707##
       $trModule
       (TrNameS "Pair"#)
       0#
       krep$*->*->*

 $krep_a2Dy [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a2Dy
   = KindRepTyConApp
       $tcPair
       (: @ KindRep $krep_a2Dv (: @ KindRep $krep_a2Dx ([] @ KindRep)))

 $krep_a2Dw [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a2Dw = KindRepFun $krep_a2Dx $krep_a2Dy

 $krep_a2Du [InlPrag=NOUSERINLINE[~]] :: KindRep
 [LclId]
 $krep_a2Du = KindRepFun $krep_a2Dv $krep_a2Dw

 $tc'Pair :: TyCon
 [LclIdX]
 $tc'Pair
   = TyCon
       13419949030541524809##
       8448108315116356699##
       $trModule
       (TrNameS "'Pair"#)
       2#
       $krep_a2Du

 *** End of Offense ***

 <no location info>: error:
 Compilation had errors

 *** Exception: ExitFailure 1
 }}}

 I've tried various combinations of `zonkTcTypes` and `zonkTcTypeToTypes`,
 but none of them work, so I'm thoroughly stuck here.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:47
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler