[GHC] #13408: Consider inferring a higher-rank kind for type synonyms
#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example: {{{#!hs f :: (forall a. a -> a -> a) -> Int f z = z 0 1 g = f }}} `g` gets an inferred type equal to `f`'s. However, this fails at the type level: {{{#!hs type F (z :: forall a. a -> a -> a) = z 0 1 type G = F }}} If anything is strange here, it's that the term-level definition is accepted. GHC should not be in the business of inferring higher-rank types. But there is an exception for definitions comprising one non- recursive equation. This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted. This is spun off from #13399, but is not tightly coupled to that ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: wontfix | 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: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => wontfix Comment: Actually, this is all bogus. In `type G = F`, `F` is undersaturated, which is disallowed. And once we write `type G z = F z`, when we're inferring a higher-rank type for `z`, we've gone further off the map than I'm comfortable with. Additionally, getting this right would require tracking recursiveness in type declarations more than we do already, and it's not worth the pain. So I'm closing as wontfix. Anyone who wants this can always add a kind signature. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: closed => new * resolution: wontfix => Comment: I talked with goldfire today about this issue, but in a slightly different context. The issue this time was that I had: {{{#!hs data A :: Type -> Type data B a :: A a -> Type }}} And I wanted to define a type synonym alias for `B`: {{{#!hs type C = B }}} This time, we came to the opposite conclusion of comment:2 — that is, GHC //should// be able to accept this. There are two main reasons why: * Unlike in the original example, in which the RHS of a type synonym was attempting to partially apply a type synonym (which is problematic), there is no problem with partially applying a data type constructor such as `B`. * The implementation might be easier than what goldfire had originally thought when writing comment:2. In the code that kind-checks type synonym declarations, we would need to check that the type synonym is the sole declaration in a mutually recursive group. (That is to say, no funny business with recursion is going on.) If this holds true, then we could grab the kind from the RHS (even if it's fancy, like the kind of `B :: forall a -> A a -> Type`) and use that to infer the kind of the whole type synonym. Having this work is especially important in the context of this particular example since there is currently no way to write the kind `forall a -> A a -> Type` in source Haskell. (If there were a way to write this, then `type C = (B :: forall a -> A a -> Type)` would already be a suitable workaround.) goldfire, please correct me if I got any details wrong here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): You got it. I do think a little twiddling in `kcTyClGroup` will get you what you want. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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): To be clear, I have no idea what "a little twiddling" constitutes in the slightest. The only clues I have are: * The [http://git.haskell.org/ghc.git/blob/0bdbbd4a637b169aa7043e0d9898ad1ecd5d14ef... code] around `Note [Single function non-recursive binding special-case]` looks relevant: {{{#!hs -- Single function binding, | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS , Nothing <- sig_fn name -- ...with no type signature = -- Note [Single function non-recursive binding special-case] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- In this very special case we infer the type of the -- right hand side first (it may have a higher-rank type) -- and *then* make the monomorphic Id for the LHS -- e.g. f = \(x::forall a. a->a) -> <body> -- We want to infer a higher-rank type for f setSrcSpan b_loc $ do { ((co_fn, matches'), rhs_ty) <- tcInferInst $ \ exp_ty -> -- tcInferInst: see TcUnify, -- Note [Deep instantiation of InferResult] tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $ -- We extend the error context even for a non-recursive -- function so that in type error messages we show the -- type of the thing whose rhs we are type checking tcMatchesFun (L nm_loc name) matches exp_ty ; ... } }}} I'm guessing that the type that you get from `tcInferInst` is important here. * [http://git.haskell.org/ghc.git/blob/849d3848f6a43c36eb0fffe45894be947ad66bfc... This] appears to be the relevant code for kind-checking type synonyms: {{{#!hs getInitialKind decl@(SynDecl { tcdLName = L _ name , tcdTyVars = ktvs , tcdRhs = rhs }) = do { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl) ktvs $ case kind_annotation rhs of Nothing -> newMetaKindVar Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig ; return [tycon] } where -- Keep this synchronized with 'hsDeclHasCusk'. kind_annotation (L _ ty) = case ty of HsParTy _ lty -> kind_annotation lty HsKindSig _ _ k -> Just k _ -> Nothing }}} If I pass in the `[LTyClDecl GhcRn]` argument from `kcTyClGroup`, I can figure out if that type synonym is part of a recursive group or not. Similarly, if `kind_annotation rhs` returns `Nothing`, then I know that we don't have a CUSK. If those two things simultaneously hold true, then I'm in a situation where we should infer the overall kind. ...except that I'm not sure at all how to go about doing so. Several mysteries have presented itself: * Where exactly should `tcInferInst` go into this? Does the type that it give you in its callback refer to the overall kind of the type synonym? Just the return kind? Something else? * Once I have access to the type in `tcInferInst`, what do I even do with it? Do I pass it to `tcLHsKindSig`? Is there another function that's better suited to this situation? * `tcInferInst` also //returns// a type. What should I do with that? * Is the `tcExtendBinderStack` stuff from the term-level code relevant to this situation? Without some kind of direction, I'm very under-qualified to fix this, I'm afraid. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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
#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): A few remarks about the code: - Put the `solveEqualities` around the first line, as the `tcLHsType` can emit constraints, and these will need to be solved. - Remove the second line. We don't need to run `kcTyClDecl` here. `kcTyClDecl`'s purpose in life is to generate constraints on the unification variables generates in `getInitialKind`. But we're not calling `getInitialKind`, so no need for `kcTyClDecl`. - Generalization looks about right. About the changed error messages: - The first will be hard to fix, for the reasons you describe. You could probably put some variant of `APromotionErr` in the env't to get a better message here. No, you can't just put the tycon in the env't, because you're making the tycon. Don't even think about `fixM` here. - The others just want for a `addTyConCtxt` around the call to `generalise`, which does a wee bit of validity checking. Otherwise, looks good! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: patch Priority: normal | Milestone: 8.8.1 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): Phab:D5301 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5301 * milestone: => 8.8.1 Comment: Alright, I've given it my best shot at Phab:D5301. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 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: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: patch => new * differential: Phab:D5301 => Comment: I made a good-faith attempt to get Phab:D5301 past the review process, but I simply couldn't muster the energy to finish it. I've abandoned Phab:D5301, although I would gladly support anyone who wishes to pick it back up again and see it to completion. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 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): I should also mention that there is actually a feasible workaround to the problem in comment:3: just use `ImpredicativeTypes`! That is to say, the following works: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} module Foo where import Data.Kind data A :: Type -> Type data B a :: A a -> Type type C = B }}} Until someone fixes this bug, I can profitably use this workaround in `singletons`, where the inability to define something like `C` was particularly irksome: https://github.com/goldfirere/singletons/pull/373 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13408: Consider inferring a higher-rank kind for type synonyms -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.10.1 Component: Compiler | Version: 8.0.1 Resolution: | Keywords: TypeInType, | VisibleDependentQuantification Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: TypeInType => TypeInType, VisibleDependentQuantification Comment: Visible dependent quantification provides another workaround for this issue: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} module Foo where import Data.Kind data A :: Type -> Type data B a :: A a -> Type type C = (B :: forall a -> A a -> Type) }}} This workaround is mildly more tolerable, since it doesn't rely on `ImpredicativeTypes`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13408#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC