[GHC] #13408: Consider inferring a higher-rank kind for type synonyms

[GHC]

#13408: Consider inferring a higher-rank kind for type synonyms
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Thanks, goldfire. With the push in comment:6, I was able to barf out this
 code:

 {{{#!diff
 diff --git a/compiler/typecheck/TcTyClsDecls.hs
 b/compiler/typecheck/TcTyClsDecls.hs
 index 5725cfd..438884b 100644
 --- a/compiler/typecheck/TcTyClsDecls.hs
 +++ b/compiler/typecheck/TcTyClsDecls.hs
 @@ -483,6 +483,19 @@ kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
  -- Third return value is Nothing if the tycon be unsaturated; otherwise,
  -- the arity
  kcTyClGroup decls
 +  | [ldecl@(L _ decl@(SynDecl { tcdLName = L _ name
 +                              , tcdTyVars = ktvs
 +                              , tcdRhs = rhs }))] <- decls
 +  , not (hsDeclHasCusk decl)
 +  = do tycon <- kcLHsQTyVars name TypeSynonymFlavour False ktvs $
 +                snd <$> tcLHsType rhs
 +       solveEqualities $ tcExtendKindEnvWithTyCons [tycon] $ kcLTyClDecl
 ldecl
 +       candidates <- gather1 tycon
 +       _ <- quantifyTyVars emptyVarSet candidates
 +       poly_tycon <- generalise tycon
 +       return [poly_tycon]
 +
 +  | otherwise
    = do  { mod <- getModule
          ; traceTc "---- kcTyClGroup ---- {" (text "module" <+> ppr mod $$
 vcat (map ppr decls))
 }}}

 Surprisingly, this actually seems to do the trick—`type C = B` actually
 typechecks with this! The code is a little messy in its current state, but
 it appears to get the job done. Surely this must be too good to be true?

 Well, it turns out it //is// too good to be true. With this patch, there
 are three test cases whose error messages degrade in quality. They are:

 * `ghc-e-fail2`:

 {{{#!diff
 diff -uw "ghc-e/should_fail/ghc-e-fail2.run/ghc-e-fail2.stderr.normalised"
 "ghc-e/should_fail/ghc-e-fail2.run/ghc-e-fail2.run.stderr.normalised"
 --- ghc-e/should_fail/ghc-e-fail2.run/ghc-e-fail2.stderr.normalised
 2018-11-03 18:35:09.522096111 -0400
 +++ ghc-e/should_fail/ghc-e-fail2.run/ghc-e-fail2.run.stderr.normalised
 2018-11-03 18:35:09.522096111 -0400
 @@ -1,4 +1,5 @@

 -<interactive>:0:1:
 -    Cycle in type synonym declarations:
 -      <interactive>:0:1-10: type A = A
 +<interactive>:0:10:
 +     Type constructor ‘A’ cannot be used here
 +        (it is defined and used in the same recursive group)
 +     In the type ‘A’
 }}}

   I think the reason this happens is because we're now calling `tcLHsType`
 before the code that perform the type-synonym cycle detection, and
 `tcLHsType` eventually invoked `promotionErr` when it sees `A` on the RHS
 (resulting in the "same recursive group" message).

   I think calling `tcExtendKindEnvWithTyCons` before `tcLHsType` would
 avoid `promotionErr` being invoked, but the problem is that the tycon that
 we need to pass `tcExtendKindEnvWithTyCons` is returned by `kcLHsQTyVars
 ... (tcLHsType rhs)` itself! So I'm stuck in a Catch-22 situation.
 * `T7433` and `T10451`:

 {{{#!diff
 diff -uw "polykinds/T7433.run/T7433.stderr.normalised"
 "polykinds/T7433.run/T7433.comp.stderr.normalised"
 --- polykinds/T7433.run/T7433.stderr.normalised 2018-11-03
 18:39:39.494098330 -0400
 +++ polykinds/T7433.run/T7433.comp.stderr.normalised    2018-11-03
 18:39:39.494098330 -0400
 @@ -3,4 +3,3 @@
       Data constructor ‘Z’ cannot be used here
          (perhaps you intended to use DataKinds)
       In the type ‘ 'Z’
 -      In the type declaration for ‘T’
 }}}
 {{{#!diff
 diff -uw "polykinds/T10451.run/T10451.stderr.normalised"
 "polykinds/T10451.run/T10451.comp.stderr.normalised"
 --- polykinds/T10451.run/T10451.stderr.normalised       2018-11-03
 18:39:39.702098331 -0400
 +++ polykinds/T10451.run/T10451.comp.stderr.normalised  2018-11-03
 18:39:39.702098331 -0400
 @@ -2,10 +2,10 @@
  T10451.hs:22:12:
      Constraint tuple arity too large: 64 (max arity = 62)
        Instead, use a nested tuple
 -    In the type ‘(Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 +     In the type ‘(Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
                    Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 Eq a, Eq a,
                    Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 Eq a, Eq a,
                    Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 Eq a, Eq a,
                    Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 Eq a, Eq a,
 -                  Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 Eq a, Eq a)’
 -    In the type declaration for ‘T’
 +                    Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a, Eq a,
 Eq a, Eq a,
 +                    Eq a)’
 }}}

   I'm not sure yet what is causing this.

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