Opened 10 months ago

Last modified 9 months ago

#12928 new feature request

Too easy to trigger CUSK condition using TH

Reported by: int-index Owned by:
Priority: high Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc:
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

While trying to make singletons class promotion work with kind-polymorphic type variables, I've encountered a problem regarding CUSKs.

Consider this class:

$(promoteOnly [d|
  class Cls a  where
    fff :: Proxy a -> ()
  |])

The generated TH (slightly simplified by hand) looks like this:

type FffSym1 (t_alvm :: Proxy a1627472612) = Fff t_alvm

data FffSym0 (l_alvn :: TyFun (Proxy a1627472612) ())

type instance Apply FffSym0 l_alvn = FffSym1 l_alvn

class PCls a_alve where
  type Fff (arg_alvl :: Proxy a_alve) :: ()

However, it fails to compile with the following error:

cusk.hs:25:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
      a1627472612 :: k0
      l_alvn :: TyFun (Proxy a1627472612) ()

As suggested by the error message, we need to specify the kind in its entirety (write a proper CUSK). So to sidestep the issue, we can write

data FffSym0 (l_alvn :: TyFun (Proxy (a1627472612 :: k)) ())

and it'll work. However, this means that the TH code generator should perform some guesswork to modify kind annotations. It sounds like a minefield — too much can go wrong, so it'd be great to avoid doing so.

Looking at the module TcHsType in the GHC sources, I see that the error is reported by the kcHsTyVarBndrs function:

          -- If there are any meta-tvs left, the user has
          -- lied about having a CUSK. Error.
       ; let (meta_tvs, good_tvs) = partition isMetaTyVar qkvs
       ; when (not (null meta_tvs)) $
         report_non_cusk_tvs (qkvs ++ tc_tvs)

However, I don't see why we can't generalize over meta_tvs instead of reporting a failure. I asked on IRC #ghc and ezyang suggested that it should be sound.

Below I attach a self-contained example that demonstrates the issue and has no dependencies except base.

Attachments (1)

cusk.hs (790 bytes) - added by int-index 10 months ago.
CUSK failure example

Download all attachments as: .zip

Change History (11)

Changed 10 months ago by int-index

Attachment: cusk.hs added

CUSK failure example

comment:1 Changed 10 months ago by goldfire

ezyang is right -- it would be sound. But it would defeat the purpose of CUSKs.

The idea with CUSKs is that they allow a user to specify when everything about the kind of a type-level definition (datatype, newtype, class, family, type synonym) is known, without any inference. When a CUSK is available, GHC can then use polymorphic recursion and other fancy features while checking the type. Without a CUSK, though, inference with polymorphic recursion is impossible.

Here is an example:

type family F (a :: k) where
  F Int = Bool

What's the kind of F? There are at least two possibilities: k -> Type and k -> k. Neither is more general than the other. Instead of guessing between these (and others that use kind families!), GHC rejects the definition as lacking a CUSK.

Is this an example of polymorphic recursion? Sort of. You can see it as polymorphic recursion if we consider that we're defining F but the occurrence of F in the equation is specialized to operate at kind Type. So it falls under this whole umbrella.

Getting back to the original question: we could generalize here. But then type inference would become unpredictable.

comment:2 Changed 10 months ago by int-index

How come we don't have a notion of "complete user-supplied type" to support polymorphic recursion at term level and still retain type inference?

Last edited 10 months ago by int-index (previous) (diff)

comment:3 Changed 10 months ago by simonpj

How come we don't have a notion of "complete user-supplied type" to support polymorphic recursion at term level and still retain type inference?

We do! It's called a type signature.

An alternative to the CUSK thing would be to provide for kind siguatures; e.g.

type D :: (* -> *) -> *
type D f = f Int

We didn't do that because at the time it seemed more syntactically invasive. But it'd make it all much clearer.

comment:4 in reply to:  3 Changed 10 months ago by int-index

Replying to simonpj:

We do! It's called a type signature.

It doesn't sound right. In a type signature, I can omit polymorphic kinds. In a CUSK, I cannot.

The example in the ticket defines a method fff which has a type signature, but a is kind-polymorphic:

  class Cls a  where
    fff :: Proxy a -> ()

comment:5 Changed 10 months ago by int-index

The offending definition has this shape:

data FffSym0 (x :: TyFun (Proxy a) ()) :: Type

and the term-level equivalent is, I believe, this:

fffSym0 :: TyFun (Proxy a) () -> Type
fffSym0 = undefined

However, one is accepted and the other is not. The inferred kind of a is a polymorphic k:

> :type fffSym0 
fffSym0 :: forall k (a :: k). TyFun (Proxy k a) () -> Type
Last edited 10 months ago by int-index (previous) (diff)

comment:6 Changed 10 months ago by simonpj

Right. In type signatures we look at the type signature all by itself, quite independent of the definition, and generalise any kind variables. So when you write

fffSym0 :: TyFun (Proxy a) () -> Type

we'll behave (as you say) as if you wrote:

fffSym0 :: forall k. forall (a:k). TyFun (Proxy a) () -> Type

I agree that this would be reasonable behaviour for a type-level kind sinature. Does everyone agree?

BUT we don't have separate type-level kind signatures (yet). If we did, yes. But as-is, do we really want to trigger generalisation when (and only when) the CUSK conditions are satisfied. Maybe so...?

comment:7 Changed 10 months ago by int-index

But isn't necessary to provide a separate type signature for fffSym0! I can write it like this using scoped type variables:

fffSym0 (x :: TyFun (Proxy a) ()) = undefined :: Type

and its type is inferred as before.

comment:8 Changed 10 months ago by int-index

Here's a complete GHCi session to demonstrate the asymmetry:

GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XTypeInType -XScopedTypeVariables 
Prelude> import Data.Proxy
Prelude Data.Proxy> import Data.Kind
Prelude Data.Proxy Data.Kind> data TyFun :: * -> * -> *
Prelude Data.Proxy Data.Kind> fffSym0 (x :: TyFun (Proxy a) ()) = undefined :: Type
Prelude Data.Proxy Data.Kind> :type fffSym0 
fffSym0 :: forall k (a :: k). TyFun (Proxy a) () -> Type
Prelude Data.Proxy Data.Kind> data FffSym0 (x :: TyFun (Proxy a) ()) :: Type

<interactive>:7:1: error:
    You have written a *complete user-suppled kind signature*,
    but the following variable is undetermined: k0 :: *
    Perhaps add a kind signature.
    Inferred kinds of user-written variables:
      a :: k0
      x :: TyFun (Proxy a) ()

comment:9 Changed 10 months ago by goldfire

Another way to see the difference is that GHC uses the definition of a type to inform its kinds. That is,

data T a = MkT (a Int)

will infer a :: Type -> Type.

On the other hand, term-level type signatures stand entirely on their own, as Simon says. So,

x :: forall a. Proxy a
x = Proxy :: Proxy (a :: Type)

is rejected, even though choosing a :: Type in the type signature would work here.

I've been favoring having standalone type-level kind signatures for some time, and am waiting for the right time to introduce a ghc-proposal to this end. CUSKs are terribly fiddly and very unexpected to users!

comment:10 Changed 9 months ago by simonpj

Keywords: TypeInType added
Note: See TracTickets for help on using tickets.