Opened 4 months ago

Last modified 8 weeks 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:
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 (7)

comment:1 Changed 4 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 4 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 4 months ago by Iceland_jack

Cc: Iceland_jack added

comment:4 Changed 4 months ago by goldfire

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

comment:5 Changed 3 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 2 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 8 weeks 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.

Note: See TracTickets for help on using tickets.