#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