Opened 10 months ago

Last modified 3 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 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

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.

Change History (7)

comment:1 Changed 10 months ago by RyanGlScott

Cc: RyanGlScott added

comment:2 Changed 10 months ago by simonpj

Keywords: TypeInType added

comment:3 Changed 3 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 3 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 3 months ago by RyanGlScott (previous) (diff)

comment:5 Changed 3 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 3 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 3 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]
...
Note: See TracTickets for help on using tickets.