Re: [GHC] #16008: GHC HEAD type family regression involving invisible arguments

7 Dec 2018

      #16008: GHC HEAD type family regression involving invisible arguments
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.8.1
       Component:  Compiler (Type    |              Version:  8.7
  checker)                           |             Keywords:  TypeFamilies,
      Resolution:                    |  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I haven't confirmed this yet, but I believe the culprit is
 [http://git.haskell.org/ghc.git/blob/c77fbd94cc60301e5696b75cda44adb07da19a6a...
 this part] of `tcTyFamInstEqnGuts`:

 {{{#!hs
     tc_lhs | null hs_pats  -- See Note [Apparently-nullary families]
            = do { (args, rhs_kind) <- tcInstTyBinders $
                                       splitPiTysInvisibleN (tyConArity
 fam_tc)
                                                            (tyConKind
 fam_tc)
                 ; return (mkTyConApp fam_tc args, rhs_kind) }
            | otherwise
            = tcFamTyPats fam_tc mb_clsinfo hs_pats
 }}}

 In the `null hs_pats` case, we are calling `tcInstTyBinders`, but that
 doesn't take the class-bound variables (in `mb_clsinfo`) into account!
 Some evidence which supports this theory:

 1. The `otherwise` case (when the type family takes at least one argument)
 //does// take `mb_clsinfo` into account. You can see for yourself that
 this code works correctly by observing that this variant of the original
 program typechecks:

 {{{#!hs
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind

 class C k where
   type S z :: k -> Type

 data D :: Type -> Type
 data SD :: forall a. D a -> Type

 instance C (D a) where
   type S z = SD
 }}}

 2. Before commit 2257a86daa72db382eb927df12a718669d5491f8 (`Taming the
 Kind Inference Monster`), which introduced this regression, the code that
 corresponded to `tc_lhs` was this:

 {{{#!hs
 kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
   = do { -- It's still possible the lhs_ki has some foralls. Instantiate
 these away.
          (new_pats, insted_lhs_ki)
            <- instantiateTyUntilN mb_kind_env 0 lhs_ki
 }}}

    This code uses a function which is aware of the class-bound variables
 (`mb_kind_env`).

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