[GHC] #14419: Check kinds for ambiguity
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected: {{{#!hs type family F a data T :: F a -> Type }}} `T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site. This check would be disabled by `AllowAmbiguousTypes`. Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days. This was inspired by #14203, but no need to read that ticket to understand this one. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: 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/14419#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 simonpj): * keywords: => TypeInType -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): After faec8d358985e5d0bf363bd96f23fe76c9e281f7, this is partially done. This data type's kind is currently rejected for being ambiguous: {{{#!hs type family F a data T1 :: forall a. F a -> Type }}} However, it would be premature to call this issue fixed, since the following two data types with very similar kinds are //not// rejected as ambiguous: {{{#!hs data T2 :: F a -> Type data T3 (b :: F a) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): OK, I think I know what is going on here. The reason that neither of these declarations: {{{#!hs data T2 :: F a -> Type data T3 (b :: F a) }}} Were flagged as ambiguously kinded is because `checkValidType` was only being called on the kinds of the individual arguments and result. In the former case, that would be `F a[sk] -> Type`, and in the latter case, it would be `F a[sig]`. What we need to be doing to catch the ambiguity in those cases is to call `checkValidType` on the //entire// kind of the declaration—in both cases, `forall a. F a -> Type`. I even whipped up a patch for doing so, which is essentially as simple as sticking an extra check in `kcTyClGroup`: {{{#!diff diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 7e523a7..2d4dfc5 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -535,10 +535,13 @@ kcTyClGroup decls ; checkValidTelescope all_binders user_tyvars extra -- Make sure tc_kind' has the final, zonked kind variables + ; let tc_kind' = mkTyConKind all_binders' tc_res_kind' + ; checkValidType (DeclKindCtxt name) tc_kind' + ; traceTc "Generalise kind" $ vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind) , ppr kvs, ppr all_binders, ppr tc_res_kind - , ppr all_binders', ppr tc_res_kind' + , ppr all_binders', ppr tc_res_kind', ppr tc_kind' , ppr scoped_tvs ] ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind' }}} That catches both of the examples above. But there's a gotcha that I didn't anticipate: consider these: {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F (x :: a) type family T1 (x :: a) :: F a -- Kind: forall a. a -> F a type family T2 (x :: a) :: F x -- Kind: forall a. forall (x :: a) -> F x }}} After my patch, GHC flags `T2` as ambiguous: {{{ $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180521: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:8:1: error: • Couldn't match expected type ‘F x’ with actual type ‘F x0’ NB: ‘F’ is a non-injective type family The type variable ‘x0’ is ambiguous • In the ambiguity check for the top-level kind for ‘T2’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type family declaration for ‘T2’ | 8 | type family T2 (x :: a) :: F x | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} I find this somewhat surprising, since I would expect that the `forall (x :: a)` argument in the kind of `T2` would fully determine `x`. Perhaps this is a deficiency in the code which checks for ambiguity? I tried taking a look myself, but quickly became lost, since it relies on `tcSubType_NC` (something that is completely impenetrable to me). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): Not sure offhand why you witnessed the failure that you did, but I think it's troublesome to put the ambiguity check where you did. Better would be in `checkValidTyCon`, where other validity checks are done. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 simonpj): * I agree that `checkValidTyCon` is a better place. (It's outside "the knot".) * We should ''remove'' any `checkValidType` calls on the individual kind ascriptions. No point in calling it on the `a` in `data T (x::a) = ...`. I have not looked into just where we'd remove it. Your point about the ambiguity check is very interesting. At the term level, the ambiguity check models this: {{{ f :: forall a. F a -> Int f = ... f2 :: forall a. F a -> Int f2 = f }}} It's very confusing if `f2` does not typecheck; after all, it has the same type as `f`. The ambiguity check tests this. At the call of `f` we instantiate its foralls (say `a :-> alpha`); and then unify with a skolemised version of `f2`'s type. And thus we unify `F alpha ~ F a` and fail. Analogously, suppose we said (as you suggest) {{{ type family F (x :: a) type family T2 (x :: a) :: F x -- Kind: forall a. forall (x :: a) -> F x }}} I've changed your `T2` to be a data type. Occurrences of `T2` will look like `T2 {a} x`, where the `{a}` is invisible in the source language; it is implicitly instantiate. But not that the `x` argument is fully explicit. Now type T3 :: forall a. forall (x::a) -> F x type T3 x = T2 x }}} (I know we don't have separate kind signatures yet, but we will!) Notice that we must apply `T2` to its explicit args; the `forall (x::a) -> blah` behaves like an arrow not like an (implicitly-instantiated) forall from the point of view of ambiguity checking. Looking at `TcUnify.tc_sub_type_ds`, the culprit looks like the call to `topInstantiate`. It already comes in two variants: * `topInstantiate`: instantiate all outer foralls * `topInstantiateInferred`: instantiate all outer `Inferred` foralls But the former instantiates `Required` foralls, and '''I think it should never do so.''' NB: See `Note [TyVarBndrs, TyVarBinders, TyConBinders, and visibility]` in `TyCoRep` for a refresher on `Inferred/Specified/Required`. (NB: `Required` binders never occur in the foralls of a term variable, so this change cannot affect the term level.) Richard, do you agree? Ryan, would you like to try that (a one-line change in `should_inst` in `Inst.top_instantiate`)? Richard, I must say that I find it hard to be sure where we should call `topInstantiate` and where `topInstantiateInferred`. Some comments at the call sites would be very welcome. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): Simon, is this the one-line change you had in mind? {{{#!diff diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 7b27dfa..30023b9 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -227,7 +227,7 @@ top_instantiate inst_all orig ty (theta, rho) = tcSplitPhiTy phi should_inst bndr - | inst_all = True + | inst_all = binderArgFlag bndr /= Required | otherwise = binderArgFlag bndr == Inferred deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) }}} Unfortunately, that causes `tc_sub_type_ds` to loop on `type family T2` from comment:4. The `-ddump-tc-trace` output loops on: {{{ tc_sub_type_ds ty_actual = forall (x :: a_a1zH[tau:1]) -> F x ty_expected = F x_a1zG[sk:1] Instantiating all tyvars? True origin arising from a type equality forall a. forall (x :: a) -> F x ~ forall a. forall (x :: a) -> F x type forall x_a1za. F x_a1za theta [] leave_bndrs [x_a1za] with theta: [] tc_sub_type_ds ty_actual = forall (x :: a_a1zH[tau:1]) -> F x ty_expected = F x_a1zG[sk:1] ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): Simon, Ryan, and I had a confab about all this. We discovered several new insights: * The subkinding relationship is different than the subtyping relationship. Definition: `t1 <= t2` iff there exists a way to transform a `t1` into a `t2`. That is, there exists an expression of type `t2` with a `t1`-shaped hole. (Note that `tcSubType` and friends return an `HsWrapper`, which is precisely an expression with a hole in it.) In kinds, however, the expression language is different: it is the language of types, not terms. And, critically, there is no type-level lambda. Thus, the expression-with-a-hole is more limited, meaning fewer pairs of kinds are in the subkinding relationship. * To wit, the subkinding relationship has these rules: {{{ ----------- Refl t <= t t[t'/a] <= s ----------- Inst forall a. t <= s }}} And that's it. (The `t`s above might be polytypes.) This is in contrast to the traditional subtyping relationship (e.g. bottom of Fig. 5 from the [https://www.microsoft.com/en-us/research/wp- content/uploads/2016/02/putting.pdf Practical Type Inference] paper), which has rules for skolemization and contravariance of functions. * An ambiguity check is really a check to see whether a definition can be used unambiguously, without the need for visible type application. In terms, this notion is equivalent to a reflexive sub-type check. That is, `t` is unambiguous iff `t <= t`. However, this is ''not'' true in kinds. To wit, if `F` is a type family, then `forall a. F a -> Type` is a subkind of itself according to the relation above. We thus can't use a subkinding check to implement kind-level ambiguity. * The subkinding relation is implemented in `TcHsType.checkExpectedKind` and friends, which checks a type-checked type against an expected kind. We have two tasks: 1. Document `checkExpectedKind` and friends in light of the observation that they are computing a subkinding relation. This is a simpler way to understand those functions. 2. Write a kind-level ambiguity check. This check can simply look at a kind to ensure that all quantified kind variables appear under a sequence of injective type constructors. (That is, for each quantified variable, check that there exists a path from the root of the kind tree to an occurrence of the variable passing through only injective types.) I believe we had such a check for types, once upon a time, but removed it when Simon discovered the relationship between ambiguity and the subtyping relation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): Actually, the situation in comment:4 in which a visible, dependent kind is erroneously flagged as ambiguous can occur //today//, even without that patch. Take this program, for example: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type KindOf (a :: k) = k type family F a data A (a :: Type) :: F a -> Type data Ex (x :: KindOf A) }}} {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:13:1: error: • Couldn't match type ‘F a’ with ‘F a0’ Expected type: F a -> * Actual type: F a0 -> * NB: ‘F’ is a non-injective type family The type variable ‘a0’ is ambiguous • In the ambiguity check for the kind annotation on the type variable ‘x’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes | 13 | data Ex (x :: KindOf A) | ^^^^^^^^^^^^^^^^^^^^^^^ }}} I believe this should be accepted since `KindOf A` reduces to `forall a -> F a -> Type`, and the `forall a ->` //should// uniquely determine the `a` in `F a`. Alas, GHC doesn't currently recognize this. Thankfully, the workaround for the time being is simple: just enable `AllowAmbiguousTypes`. But I'll go ahead and post this here to make it clear that this is a problem in the present, and not just a problem for a future GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): We have no business at all running today's type-oriented ambiguity check on kinds, as they have different subtyping relations. So we have task 3. Make sure not to ever run the type-ambiguity check on kinds. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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: | -------------------------------------+------------------------------------- Description changed by goldfire: Old description:
GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected:
{{{#!hs type family F a data T :: F a -> Type }}}
`T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site.
This check would be disabled by `AllowAmbiguousTypes`.
Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days.
This was inspired by #14203, but no need to read that ticket to understand this one.
New description: GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected: {{{#!hs type family F a data T :: F a -> Type }}} `T`'s kind is ambiguous, and any occurrence of `T` will be rejected. Instead of rejecting usage sites, let's just reject the definition site. This check would be disabled by `AllowAmbiguousTypes`. Happily, I think the implementation should be easy, and that the current algorithm to check for ambiguous types should work for kinds, too. After all, types and kinds are the same these days. This was inspired by #14203, but no need to read that ticket to understand this one. EDIT: See comment:8 and comment:10 for the nub of what needs to be done here. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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 simonpj):
Make sure not to ever run the type-ambiguity check on kinds.
Do we need to do anything else instead? Or are you saying simply drop it. And if so why do the ills of ambiguous types not apply to kinds? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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): We ''do'' need an ambiguity check on kinds, but that's already accounted- for in task 2 in comment:8. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.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: Here is how to trigger the same issue using visible dependent quantification: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type family F a data Ex (x :: forall a -> F a -> Type) }}} {{{ GHCi, version 8.9.20190227: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:10:1: error: • Couldn't match type ‘F a’ with ‘F a0’ Expected type: F a -> * Actual type: F a0 -> * NB: ‘F’ is a non-injective type family The type variable ‘a0’ is ambiguous • In the ambiguity check for the kind annotation on the type variable ‘x’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the data type declaration for ‘Ex’ | 10 | data Ex (x :: forall a -> F a -> Type) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC