Opened 2 years ago
Last modified 7 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, CUSKs, GHCProposal | 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)
Change History (14)
Changed 2 years ago by
comment:1 Changed 2 years ago by
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 2 years ago by
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?
comment:3 follow-up: 4 Changed 2 years ago by
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 Changed 2 years ago by
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 2 years ago by
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
comment:6 Changed 2 years ago by
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 2 years ago by
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 2 years ago by
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 2 years ago by
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 2 years ago by
Keywords: | TypeInType added |
---|
comment:11 Changed 8 months ago by
Keywords: | CUSKs added |
---|
comment:12 Changed 7 months ago by
Cc: | GHCProposal added |
---|
See https://github.com/ghc-proposals/ghc-proposals/pull/54 for the GHC proposal alluded to in comment:9.
comment:13 Changed 7 months ago by
Cc: | GHCProposal removed |
---|---|
Keywords: | GHCProposal added |
CUSK failure example