#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 goldfire): It's just a little twiddling! How hard could it be? :) You ask good questions. But your first guesses are off: - `tcInferInst` is the right notional idea, but not a function you would actually use here. - `getInitialKind` looks at the "left-hand side" of a type declaration and invents a skeleton for the type's kind. (Example: from `data T a (b :: Type -> Type) c`, it guesses `T :: kappa1 -> (Type -> Type) -> kappa2 -> Type` for fresh unification variables `kappa1` and `kappa2`.) Because you don't need to guess the kind, it's not what you want here. What you need to do is to bring the type variables on the LHS into scope (with either guessed or provided kinds), kind-check the RHS, and then say that the LHS's kind is the same as the RHS's. Here is some direction to how to do so: - Have a special case in `kcTyClGroup` that detects a single type synonym. Type synonyms cannot be recursive, so we don't have to worry about that. (Or maybe we do, because we detect recursion in type synonyms later, perhaps? If that's the case, the renamer may want to either reject recursive type synonyms or remember the recursiveness using a new field in the AST.) - `kcLHsQTyVars` brings the LHS tyvars into scope, with appropriate kinds. Claim that the type does ''not'' have a CUSK. (Even if it ''does'' have a CUSK, CUSKness can matter only with recursion.) - `tcLHsType` does a nice job of checking the type itself -- but you'll need only the kind here, not the type. - You'll need to skolemise and quantify, much like the main branch of `kcTyClGroup`. Does that give enough guidance? I do think that, actually, we can do better here. The plan above would still have GHC take two passes over these special type synonyms, when really we can do it in one pass. But the infrastructure isn't set up for that, so it would take a more significant refactoring. Still I think the plan above is an improvement over the status quo. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler