Core Lint error with LiberalTypeSynonyms

changed milestone to %8.8.1

changed weight to 5

Is it just me, or does this Core Lint check seem entirely bogus? This seems to assume that the body of a forall will always be *-kinded, but that's just blatantly false (forall (f :: Type -> Type). f is another counterexample.)

No, the Lint check is right. The kinding rules for types are given in #15979 of #15791 (closed). And, I assume, in docs/core-spec.

So the bug is in the type checker which should reject the program. It's not easy to do that for type inference, because we lack a constraint that says "This kind should be either (TYPE r) or Constraint".

I think the easiest way to fix this would be in checkValidType; and specifically in the code you have just been working on in check_type. In a sigma-type (the code you moved up) add a test that the kind of the body is TYPE r or Constraint.

Richard, right?

Uh... what? I must be living in a different reality, then, since GHC has always let me do this without complaint:

type Foo = forall (f :: Type -> Type). f

So either I'm taking crazy pills, or those kinding rules for types are blatantly wrong.

Let's ask Richard, but I think it should never have accepted that

Another one:

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Bug where

import Data.Kind

type Foo = forall (f :: Type -> Type). f

f :: Foo Int -> Foo Int
f x = x

$ /opt/ghc/8.6.2/bin/ghc Bug.hs -dcore-lint
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the type ‘Foo Int -> Foo Int’
    Non-*-like kind when *-like expected: * -> *
    when checking the body of forall: forall (f :: * -> *). f
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)

f :: Foo Int -> Foo Int
[LclIdX]
f = \ (x_aWa :: Foo Int) -> x_aWa
end Rec }

*** End of Offense ***


<no location info>: error: 
Compilation had errors

This //passes// -dcore-lint, however:

{-# LANGUAGE RankNTypes #-}
module Works where

f :: (forall. Maybe) a
f = Nothing

forall (f :: Type -> Type). f is bogus. It should be rejected both by the type checker and Core Lint. This is rather awkward w.r.t. type inference (as Simon points out) because of Constraint. I don't like the validity-checking solution, because then we reject something like :k forall a. a in GHCi. a's kind will be unconstrained, so it will get kind k. But then the forall is bogus. We could imagine a magic class TypeLike with instance TypeLike (TYPE r) and instance TypeLike Constraint. We can further imagine defaulting this class (not unlike how we default Num). But this is a sledgehammer of a solution, to be sure.

I don't think there is anything unsound about removing the restriction... but no published type theory (to my knowledge) does so. Back in the day, the restriction wasn't there because we needed, e.g., forall a. Array# a -- that is, we needed unlifted types (which didn't really have kinds) in foralls. Now with levity polymorphism, we have a more principled way of dealing with this all, and so we do. Perhaps the new principles weren't carried all the way to their logical conclusion, though, as this ticket shows.

Note: if we really can't come up with a good way to impose this restriction in the type-checker, I wouldn't be strongly opposed to just dropping it. It's just a little smelly, but no worse than that.

Interestingly, there appears to be some sort of check for this already, but only when kind-checking. Given this:

data P k :: k -> Type

Then GHC accept the following:

type Foo = forall k (a :: k). P k a

However, it does //not// accept the following:

type Bar = forall k. P k

$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:10:22: error:
    • Expected kind ‘k0’, but ‘P k’ has kind ‘k -> *’
    • In the type ‘forall k. P k’
      In the type declaration for ‘Bar’
   |
10 | type Bar = forall k. P k
   |                      ^^^

The current error message doesn't really give a clear indication as to the underlying cause, however.

I think ticket:15979#comment:165434 is quite a separate matter: see the kinding rule for foralls in #15791 (closed)

changed milestone to %8.10.1

Bumping milestones of low-priority tickets.

added compiler crash label

Ah, it turns out that there is a Note which describes the reasoning behind the current design in TcHsType:

Note [Body kind of a HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The body of a forall is usually a type, but in principle
there's no reason to prohibit *unlifted* types.
In fact, GHC can itself construct a function with an
unboxed tuple inside a for-all (via CPR analysis; see
typecheck/should_compile/tc170).

Moreover in instance heads we get forall-types with
kind Constraint.

It's tempting to check that the body kind is either * or #. But this is
wrong. For example:

  class C a b
  newtype N = Mk Foo deriving (C a)

We're doing newtype-deriving for C. But notice how `a` isn't in scope in
the predicate `C a`. So we quantify, yielding `forall a. C a` even though
`C a` has kind `* -> Constraint`. The `forall a. C a` is a bit cheeky, but
convenient. Bottom line: don't check for * or # here.

The existence of types like forall a. C a when typechecking deriving clauses is indeed tricky. I don't know how we could check that a forall type has kind TYPE r or Constraint while simultaneously permitting these.

I've tried two different approaches to fix this bug:

Change the TcHsType.tc_hs_type case for HsForAllTy so that it checks that the body of a forall is of kind TYPE r. (This check should be skipped if the body has kind k1 -> k2 -> ... -> Constraint, for the reasons described in #15979 (comment 211378).)
Implement an additional check in TcValidity.check_type that checks if the body of a forall is of kind TYPE r or Constraint.

Unfortunately, each approach has its own issues:

It's actually rather difficult to tell in general if an LHsType GhcRn is going to have kind k1 -> k2 -> ... -> Constraint before it is typechecked (at which point it is too late). The approach that the tc_hs_type case for HsQualTy takes is to look at exp_kind to see if it is Constraint. This is not terribly robust, however, since there are certain situations where the exp_kind isn't known to be Constraint. In particular, this fails to properly work on the T11768 and T14332 test cases, which use deriving clauses of the form deriving (forall a. C a).
Putting an extra check in check_type catches some foralls that don't have kind TYPE r/Constraint, but annoyingly, it doesn't work for the test case in the original issue description. This is because when LiberalTypeSynonyms is enabled, check_type is only called on types after type synonyms have been expanded. (See Note [Correctness and performance of type synonym validity checking] in TcValidity for why things are done this way.)

It might be possible to make this approach work if we tweak the Core Lint check such that it only fires after type synonyms have been expanded when LiberalTypeSynonyms is enabled, similarly to how check_type does things.

To be, the question is: What is the specification of -XLiberalTypeSynonyms? The manual says that it does not do validity checking. According to that specification, the original program should be rejected. It contains a kind error (according to our type system), not a validity error.

Let's suppose that the deriving issue didn't exist for a moment. Would approach (1) work? I would hope so.

We really shouldn't be type-checking forall a. C a in that deriving clause. Instead, we should bring a into scope and then check C a. No forall. I don't think this should be hard.

(Also, the manual page for -XLiberalTypeSynonyms is out of date. Unboxed tuples are no longer a special case, now that we have levity-polymorphism and can assign correct kinds to unlifted things.)

We really shouldn't be type-checking forall a. C a in that deriving clause. Instead, we should bring a into scope and then check C a. No forall. I don't think this should be hard.

Do you mind expanding a little more on what you had in mind to accomplish this? I imagine one could use splitLHsSigmaTyInvis to carve out the C a part of forall a. C a. Once I do that, however, how do I bring the a (which is an LHsTyVarBndr) into scope?

Can you point me to the code you're looking at?

In the example in that Note, the user has not written a forall. So I assume that GHC is using its HsImplicitBinders. Some code has to then process these implicit binders. I'm saying that that code should not treat the implicit binders as a forall.

I do seem to remember that we allow an explicit forall in deriving clauses. In that case, before processing the clause, we should split the forall (the user doesn't really want forall; they just want to bring a variable into scope) and then treat it all like the first case.

Does that help?

Trac field	Value
Version	8.6.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

Core Lint error with LiberalTypeSynonyms

Child items ...

Activity

Core Lint error with LiberalTypeSynonyms

Relates to

Activity