Opened 14 months ago

Last modified 6 weeks ago

#14419 new bug

Check kinds for ambiguity

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.2.1
Keywords: TypeInType 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 goldfire)

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 (13)

comment:1 Changed 14 months ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 14 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 7 months ago by RyanGlScott

After faec8d358985e5d0bf363bd96f23fe76c9e281f7, this is partially done. This data type's kind is currently rejected for being ambiguous:

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:

data T2 :: F a -> Type
data T3 (b :: F a)

comment:4 Changed 7 months ago by RyanGlScott

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 
    535535           ; checkValidTelescope all_binders user_tyvars extra
    536536
    537537                      -- 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
    538541           ; traceTc "Generalise kind" $
    539542             vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
    540543                  , 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'
    542545                  , ppr scoped_tvs ]
    543546
    544547           ; 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/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).

Last edited 7 months ago by RyanGlScott (previous) (diff)

comment:5 Changed 7 months ago 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.

comment:6 Changed 7 months ago 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.

comment:7 Changed 7 months ago by RyanGlScott

Simon, is this the one-line 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 
    227227    (theta, rho)   = tcSplitPhiTy phi
    228228
    229229    should_inst bndr
    230       | inst_all  = True
     230      | inst_all  = binderArgFlag bndr /= Required
    231231      | otherwise = binderArgFlag bndr == Inferred
    232232
    233233deeplyInstantiate :: 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]
...

comment:8 Changed 3 months ago 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 ts 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 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.
  1. 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.

comment:9 Changed 6 weeks ago 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:

{-# 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.

comment:10 Changed 6 weeks ago 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

  1. Make sure not to ever run the type-ambiguity check on kinds.

comment:11 Changed 6 weeks ago by goldfire

Description: modified (diff)

comment:12 Changed 6 weeks ago 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?

comment:13 Changed 6 weeks ago by goldfire

We do need an ambiguity check on kinds, but that's already accounted-for in task 2 in comment:8.

Note: See TracTickets for help on using tickets.