Opened 2 years ago
Last modified 11 months ago
#14419 new bug
Check kinds for ambiguity
Reported by:  goldfire  Owned by:  

Priority:  normal  Milestone:  
Component:  Compiler  Version:  8.2.1 
Keywords:  TypeInType, VisibleDependentQuantification  Cc:  RyanGlScott 
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 (last modified by )
GHC does an ambiguity check on types. It should also do the same for kinds. Here is a program that should be rejected:
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.
Change History (14)
comment:1 Changed 2 years ago by
Cc:  RyanGlScott added 

comment:2 Changed 2 years ago by
Keywords:  TypeInType added 

comment:3 Changed 21 months ago by
comment:4 Changed 20 months ago by
OK, I think I know what is going on here. The reason that neither of these declarations:
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]
/Type
.
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
:

compiler/typecheck/TcTyClsDecls.hs
diff git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 7e523a7..2d4dfc5 100644
a b kcTyClGroup decls 535 535 ; checkValidTelescope all_binders user_tyvars extra 536 536 537 537  Make sure tc_kind' has the final, zonked kind variables 538 ; let tc_kind' = mkTyConKind all_binders' tc_res_kind' 539 ; checkValidType (DeclKindCtxt name) tc_kind' 540 538 541 ; traceTc "Generalise kind" $ 539 542 vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind) 540 543 , ppr kvs, ppr all_binders, ppr tc_res_kind 541 , ppr all_binders', ppr tc_res_kind' 544 , ppr all_binders', ppr tc_res_kind', ppr tc_kind' 542 545 , ppr scoped_tvs ] 543 546 544 547 ; 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:
{# 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/ghcstage2 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 noninjective type family The type variable ‘x0’ is ambiguous • In the ambiguity check for the toplevel 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).
comment:5 Changed 20 months ago by
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.
comment:6 Changed 20 months ago by
 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 thea
indata 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 (implicitlyinstantiated) 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 forallstopInstantiateInferred
: instantiate all outerInferred
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 oneline 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.
comment:7 Changed 20 months ago by
Simon, is this the oneline change you had in mind?

compiler/typecheck/Inst.hs
diff git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 7b27dfa..30023b9 100644
a b top_instantiate inst_all orig ty 227 227 (theta, rho) = tcSplitPhiTy phi 228 228 229 229 should_inst bndr 230  inst_all = True230  inst_all = binderArgFlag bndr /= Required 231 231  otherwise = binderArgFlag bndr == Inferred 232 232 233 233 deeplyInstantiate :: CtOrigin > TcSigmaType > TcM (HsWrapper, TcRhoType)
Unfortunately, that causes tc_sub_type_ds
to loop on type family T2
from comment:4. The ddumptctrace
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] ...
comment:8 Changed 16 months ago by
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 at1
into at2
. That is, there exists an expression of typet2
with at1
shaped hole. (Note thattcSubType
and friends return anHsWrapper
, 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 typelevel lambda. Thus, the expressionwithahole 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 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 subtype check. That is,
t
is unambiguous ifft <= t
. However, this is not true in kinds. To wit, ifF
is a type family, thenforall a. F a > Type
is a subkind of itself according to the relation above. We thus can't use a subkinding check to implement kindlevel ambiguity.
 The subkinding relation is implemented in
TcHsType.checkExpectedKind
and friends, which checks a typechecked type against an expected kind.
We have two tasks:
 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.
 Write a kindlevel 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.
comment:9 Changed 15 months ago by
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:
{# 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 noninjective 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.
comment:10 Changed 15 months ago by
We have no business at all running today's typeoriented ambiguity check on kinds, as they have different subtyping relations.
So we have task
 Make sure not to ever run the typeambiguity check on kinds.
comment:11 Changed 15 months ago by
Description:  modified (diff) 

comment:12 Changed 15 months ago by
Make sure not to ever run the typeambiguity 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?
comment:13 Changed 15 months ago by
We do need an ambiguity check on kinds, but that's already accountedfor in task 2 in comment:8.
comment:14 Changed 11 months ago by
Keywords:  VisibleDependentQuantification added 

Here is how to trigger the same issue using visible dependent quantification:
{# 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 noninjective 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)  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
After faec8d358985e5d0bf363bd96f23fe76c9e281f7, this is partially done. This data type's kind is currently rejected for being ambiguous:
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: