Opened 6 months ago

Last modified 12 days ago

#14887 new bug

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:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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: http://www.haskell.org/ghc/  :? 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 (13)

comment:1 Changed 6 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: http://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:
    • 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 6 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 6 months ago by Iceland_jack

Cc: Iceland_jack added

comment:4 Changed 6 months ago by goldfire

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

comment:5 Changed 5 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: http://www.haskell.org/ghc/  :? 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 4 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 4 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 3 weeks ago by RyanGlScott

Milestone: 8.8.1

comment:9 Changed 3 weeks ago by simonpj

Richard?

comment:10 Changed 3 weeks 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 3 weeks 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 3 weeks 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 12 days 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: http://www.haskell.org/ghc/  :? 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?)

Note: See TracTickets for help on using tickets.