Opened 12 months ago

Closed 3 months ago

#14887 closed bug (fixed)

Explicitly quantifying a kind variable causes a telescope to fail to kind-check

Reported by: RyanGlScott Owned by: goldfire
Priority: normal Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.2.2
Keywords: TypeInType Cc: Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: indexed-types/should_fail/T14887, polykinds/T14887a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


Consider the following program:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where

import Data.Kind
import Data.Type.Equality

type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
  Foo1 (e :: a :~: a) = a :~: a

type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
  Foo2 k (e :: a :~: a) = a :~: a

Foo2 is wholly equivalent to Foo1, except that in Foo2, the k kind variable is explicitly quantified. However, Foo1 typechecks, but Foo2 does not!

$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.2:  :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:13:10: error:
    • Couldn't match kind ‘k’ with ‘k1’
      When matching the kind of ‘a’
      Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
    • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
      In the type family declaration for ‘Foo2’
13 |   Foo2 k (e :: a :~: a) = a :~: a
   |          ^^^^^^^^^^^^^^

(Moreover, there seems to be a tidying bug, since GHC claims that (:~:) k a a is not the same kind as (:~:) k a a.)

Change History (15)

comment:1 Changed 12 months ago by RyanGlScott

A slight twist on this is if you leave out the type family equations. For instance:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where

import Data.Kind
import Data.Proxy

type family Foo1             (e :: Proxy (a :: k)) :: Type where {}
type family Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type where {}

Foo1 typechecks, but Foo2 does not:

$ ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.2:  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:10:1: error:
    • These kind and type variables: k (e :: Proxy k a)
      are out of dependency order. Perhaps try this ordering:
        k (a :: k) (e :: Proxy k a)
      NB: Implicitly declared kind variables are put first.
    • In the type family declaration for ‘Foo2’
10 | type family Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type where {}
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I have no idea why GHC is complaining about the scoping order here—that looks well-scoped to me!

comment:2 Changed 12 months ago by simonpj

Owner: set to goldfire

Interesting bug, thanks. But not much point in looking at this until Richard's "solveEqualities" patch lands. Richard?

comment:3 Changed 12 months ago by Iceland_jack

Cc: Iceland_jack added

comment:4 Changed 12 months ago by goldfire

That patch is held up on the #12919 patch, which is under review at Phab:D4451.

comment:5 Changed 11 months ago by RyanGlScott

The #12919 patch has landed. Interestingly, the program in comment:1 now gives a different error:

$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180403:  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:10:43: error:
    • Expected kind ‘k’, but ‘a’ has kind ‘k0’
    • In the first argument of ‘Proxy’, namely ‘(a :: k)’
      In the kind ‘Proxy (a :: k)’
10 | type family Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type where {}
   |                                           ^

comment:6 Changed 10 months ago by RyanGlScott

Keywords: TypeFamilies removed
Summary: Explicitly quantifying a kind variable causes a type family to fail to typecheckExplicitly quantifying a kind variable causes a telescope to fail to kind-check

As it turns out, this is not at all specific to type families. The same phenomenon occurs in data types:

data Foo1             (e :: Proxy (a :: k)) :: Type -- typechecks
data Foo2 (k :: Type) (e :: Proxy (a :: k)) :: Type -- doesn't typecheck

Or even plain old functions:

foo1 :: forall (e :: Proxy (a :: k)).
        Int -- typechecks
foo1 = 42

foo2 :: forall (k :: Type) (e :: Proxy (a :: k)).
        Int -- doesn't typecheck
foo2 = 42

So I'm guessing that any type variable telescope suffers from this issue.

comment:7 Changed 10 months ago by simonpj

Here's what is going on with:

foo2 :: forall (k :: Type) (e :: Proxy (a :: k)). Int

In TcHsType.tc_hs_sig_type_and_gen we see

tc_hs_sig_type_and_gen skol_info (HsIB { hsib_vars = sig_vars
                                       , hsib_body = hs_ty }) kind
  = do { (tkvs, ty) <- solveEqualities $
                       tcImplicitTKBndrs skol_info sig_vars $
                       tc_lhs_type typeLevelMode hs_ty kind

Here sig_vars is just a. Now tcImplicitTKBndrs gives a a kind k0 (a unification variable), so we attempt to kind-check

   forall (a::k0). forall (k :: Type) (e :: Proxy (a :: k)). Int

But that requires k0 ~ k, which is a skolem-escape problem. We end up trying (and failing) solve the constraint

Implic {
  TcLevel = 2
  Skolems = (a_avH[sk:2] :: k_aZs[tau:2])
  No-eqs = True
  Status = Unsolved
  Given =
  Wanted =
    WC {wc_impl =
          Implic {
            TcLevel = 3
            Skolems = k_aZp[sk:3]
                      (e_aZq[sk:3] :: Proxy
                                        k_aZp[sk:3] (a_avH[sk:2] |> {co_aZC}))
            No-eqs = True
            Status = Unsolved
            Given =
            Wanted =
              WC {wc_simple =
                    [WD] hole{co_aZC} {0}:: (k_aZs[tau:2] :: *)
                                            GHC.Prim.~# (k_aZp[sk:3] :: *) (CNonCanonical)}

Here k0 is k_aZs, and it is (rightly) untouchable inside the level-3 implication. Hence the error message.

I have not yet thought about what to do. Richard may have some ideas.

comment:8 Changed 7 months ago by RyanGlScott

Milestone: 8.8.1

comment:9 Changed 7 months ago by simonpj


comment:10 Changed 7 months ago by simonpj

Principle: implicitly-quantified variables always precede explicitly-quantified variables in a type or kind. So Foo1 and Foo2 in the OP are not equivalent.

  • In Foo1 the implicitly-quantified variables are k and a::k; and GHC can put them in that order.
  • But in Foo2 the implicitly quantified variable is only a::k and that can't come first.

comment:11 Changed 7 months ago by simonpj

Richard's patch says

"The error message for dependent/should_fail/TypeSkolEscape has become noticeably worse. However, this is because the code in TcErrors goes to some length to preserve pre-8.0 error messages for kind errors. It's time to rip off that plaster and get rid of much of the kind-error-specific error messages. I tried this, and doing so led to a lovely error message for TypeSkolEscape. So: I'm accepting the error message quality regression for now, but will open up a new ticket to fix it, along with a larger error-message improvement I've been pondering. This applies also to dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142."

We think this is related.

comment:12 Changed 7 months ago by goldfire

I think the best way to get good error messages here is to bring both implicit and explicit variables into scope all at once, and then have setImplicationStatus report errors involving both explicit and implicit variables. See Note [Keeping scoped variables in order: Explicit] in TcHsType for the general idea; here, I'm proposing this plan to cover implicit variables, too.

One wrinkle: datatypes go via a different mechanism, in kcLHsQTyVars and friends. Question: could we unify these mechanisms?

comment:13 Changed 6 months ago by RyanGlScott

I've found another bizarre case where implicitly quantifying a kind variable works, but explicitly quantifying it does not. Consider the following program:

{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module Bug where

import Data.Proxy

f :: forall (x :: a). Proxy (x :: _)
f = Proxy

This typechecks, but if I change the type signature of f to explicitly quantify a:

f :: forall a (x :: a). Proxy (x :: _)

Then it no longer typechecks! Here is the error you get an a somewhat recent GHC HEAD build:

GHCi, version 8.7.20180802:  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )

Bug.hs:9:32: error:
    • Expected kind ‘a’, but ‘x’ has kind ‘a1’
    • In the first argument of ‘Proxy’, namely ‘(x :: _)’
      In the type ‘Proxy (x :: _)’
      In the type signature: f :: forall a (x :: a). Proxy (x :: _)
9 | f :: forall a (x :: a). Proxy (x :: _)
  |                                ^

Do you think that this shares a symptom in common with the other programs mentioned in this ticket? (Or is this a separate bug?)

comment:14 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In 2257a86d/ghc:

Taming the Kind Inference Monster

My original goal was (Trac #15809) to move towards using level numbers
as the basis for deciding which type variables to generalise, rather
than searching for the free varaibles of the environment.  However
it has turned into a truly major refactoring of the kind inference

Let's deal with the level-numbers part first:

* Augment quantifyTyVars to calculate the type variables to
  quantify using level numbers, and compare the result with
  the existing approach.  That is; no change in behaviour,
  just a WARNing if the two approaches give different answers.

* To do this I had to get the level number right when calling
  quantifyTyVars, and this entailed a bit of care, especially
  in the code for kind-checking type declarations.

* However, on the way I was able to eliminate or simplify
  a number of calls to solveEqualities.

This work is incomplete: I'm not /using/ level numbers yet.
When I subsequently get rid of any remaining WARNings in
quantifyTyVars, that the level-number answers differ from
the current answers, then I can rip out the current
"free vars of the environment" stuff.

Anyway, this led me into deep dive into kind inference for type and
class declarations, which is an increasingly soggy part of GHC.
Richard already did some good work recently in

   commit 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3
   Date:   Thu Sep 13 09:56:02 2018 +0200

    Finish fix for #14880.

    The real change that fixes the ticket is described in
    Note [Naughty quantification candidates] in TcMType.

but I kept turning over stones. So this patch has ended up
with a pretty significant refactoring of that code too.

Kind inference for types and classes

* Major refactoring in the way we generalise the inferred kind of
  a TyCon, in kcTyClGroup.  Indeed, I made it into a new top-level
  function, generaliseTcTyCon.  Plus a new Note to explain it
  Note [Inferring kinds for type declarations].

* We decided (Trac #15592) not to treat class type variables specially
  when dealing with Inferred/Specified/Required for associated types.
  That simplifies things quite a bit. I also rewrote
  Note [Required, Specified, and Inferred for types]

* Major refactoring of the crucial function kcLHsQTyVars:
  I split it into
       kcLHsQTyVars_Cusk  and  kcLHsQTyVars_NonCusk
  because the two are really quite different. The CUSK case is
  almost entirely rewritten, and is much easier because of our new
  decision not to treat the class variables specially

* I moved all the error checks from tcTyClTyVars (which was a bizarre
  place for it) into generaliseTcTyCon and/or the CUSK case of
  kcLHsQTyVars.  Now tcTyClTyVars is extremely simple.

* I got rid of all the all the subtleties in tcImplicitTKBndrs. Indeed
  now there is no difference between tcImplicitTKBndrs and
  kcImplicitTKBndrs; there is now a single bindImplicitTKBndrs.
  Same for kc/tcExplicitTKBndrs.  None of them monkey with level
  numbers, nor build implication constraints.  scopeTyVars is gone
  entirely, as is kcLHsQTyVarBndrs. It's vastly simpler.

  I found I could get rid of kcLHsQTyVarBndrs entirely, in favour of
  the bnew bindExplicitTKBndrs.

* I now deal with the "naughty quantification candidates"
  of the previous patch in candidateQTyVars, rather than in
  quantifyTyVars; see Note [Naughty quantification candidates]
  in TcMType.

  I also killed off closeOverKindsCQTvs in favour of the same
  strategy that we use for tyCoVarsOfType: namely, close over kinds
  at the occurrences.

  And candidateQTyVars no longer needs a gbl_tvs argument.

* Passing the ContextKind, rather than the expected kind itself,
  to tc_hs_sig_type_and_gen makes it easy to allocate the expected
  result kind (when we are in inference mode) at the right level.

Type families
* I did a major rewrite of the impenetrable tcFamTyPats. The result
  is vastly more comprehensible.

* I got rid of kcDataDefn entirely, quite a big function.

* I re-did the way that checkConsistentFamInst works, so
  that it allows alpha-renaming of invisible arguments.

* The interaction of kind signatures and family instances is tricky.
    Type families: see Note [Apparently-nullary families]
    Data families: see Note [Result kind signature for a data family instance]
                   and Note [Eta-reduction for data families]

* The consistent instantation of an associated type family is tricky.
  See Note [Checking consistent instantiation] and
      Note [Matching in the consistent-instantation check]
  in TcTyClsDecls.  It's now checked in TcTyClsDecls because that is
  when we have the relevant info to hand.

* I got tired of the compromises in etaExpandFamInst, so I did the
  job properly by adding a field cab_eta_tvs to CoAxBranch.
  See Coercion.etaExpandCoAxBranch.

tcInferApps and friends
* I got rid of the mysterious and horrible ClsInstInfo argument
  to tcInferApps, checkExpectedKindX, and various checkValid
  functions.  It was horrible!

* I got rid of [Type] result of tcInferApps.  This list was used
  only in tcFamTyPats, when checking the LHS of a type instance;
  and if there is a cast in the middle, the list is meaningless.
  So I made tcInferApps simpler, and moved the complexity
  (not much) to tcInferApps.

  Result: tcInferApps is now pretty comprehensible again.

* I refactored the many function in TcMType that instantiate skolems.

Smaller things

* I rejigged the error message in checkValidTelescope; I think it's
  quite a bit better now.

* checkValidType was not rejecting constraints in a kind signature
     forall (a :: Eq b => blah). blah2
  That led to further errors when we then do an ambiguity check.
  So I make checkValidType reject it more aggressively.

* I killed off quantifyConDecl, instead calling kindGeneralize

* I fixed an outright bug in tyCoVarsOfImplic, where we were not
  colleting the tyvar of the kind of the skolems

* Renamed ClsInstInfo to AssocInstInfo, and made it into its
  own data type

* Some fiddling around with pretty-printing of family
  instances which was trickier than I thought.  I wanted
  wildcards to print as plain "_" in user messages, although
  they each need a unique identity in the CoAxBranch.

Some other oddments

* Refactoring around the trace messages from reportUnsolved.
* A bit of extra tc-tracing in TcHsSyn.commitFlexi

This patch fixes a raft of bugs, and includes tests for them.

 * #14887
 * #15740
 * #15764
 * #15789
 * #15804
 * #15817
 * #15870
 * #15874
 * #15881

comment:15 Changed 3 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T14887, polykinds/T14887a
Note: See TracTickets for help on using tickets.