Type checker crash

changed the description

This is very awkward. Notice that FunctionSymbol is a phantom type synonym. So given the separate kind signature

type IsSum :: forall s. FunctionSymbol s -> Constraint

we don't have a way to match up the s in the signature with the t in

class IsSum (sumf :: FunctionSymbol t) where

because FunctionSymbol t is phantom. Indeed maybe you could say

class IsSum (sumf :: FunctionSymbol (p,q)) where

Yuk. This is very much a corner case. I rather think that we should error if a pattern-signature-bound type variable occurs only under a type synonym.

Perhaps that rule should apply more generally. Consider this

type FS t = Int

f :: Int -> Bool
f (x :: FS a) = True :: a

THis is actually accepted today. a is bound to a unification variable, wich ultimately turns out to be Bool. But that is pretty horrible. And in the context of kind-checking a class decl with a separaet kind signature, it is not easy to "just make it a unification variable".

For now I propose to make this situation (which occurs only with standalone kind signatures) error saying something like:

   Type variable `t` is not determined by the standalone kind signature.
   (Perhaps it appears only under a type synonym.)

Any views @rae @sheaf?

I'm somewhat surprised by this conclusion. I was under the impression that this:

class IsSum (sumf :: FunctionSymbol t) where

Was syntactic sugar for this:

class IsSum @t (sumf :: FunctionSymbol t) where

And GHC already knows how to match up the s in type IsSum :: forall s. ... with class IsSum @t .... In fact, this does work:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeAbstractions #-}

type IsSum :: forall s. FunctionSymbol s -> Constraint
-- Note the explicit @t
class IsSum @t (sumf :: FunctionSymbol t) where
    sumConNames :: Pi t

So why does leaving off the @t make a difference?

What about

class IsSum (sumf :: FunctionSymbol (Int,t)) where
    sumConNames :: Pi t

And what order would you like the variables in? Is

class IsSum (sumf :: FunctionSymbol (p,q)) where

short for

class IsSum @p @q (sumf :: FunctionSymbol (p,q)) where

or

class IsSum @q @p (sumf :: FunctionSymbol (p,q)) where

Rememeber, FunctionSymbol just tosses away its argument.

What about

class IsSum (sumf :: FunctionSymbol (Int,t)) where
    sumConNames :: Pi t

I'm not sure what to remark on here, other than to say that that should be syntactic sugar for:

class IsSum @t (sumf :: FunctionSymbol (Int,t)) where ...

And now the same reasoning as above applies.

And what order would you like the variables in? Is
class IsSum (sumf :: FunctionSymbol (p,q)) where
short for
class IsSum @p @q (sumf :: FunctionSymbol (p,q)) where
or
class IsSum @q @p (sumf :: FunctionSymbol (p,q)) where
Rememeber, FunctionSymbol just tosses away its argument.

The specification in this section of the GHC User's Guide would suggest that the only correct answer is @p @q. The specification says nothing about "tossing away arguments", which I think is a good thing, since I think the order of type variables should be apparent with a simple syntactic traversal over the definition, without caring about things such as type synonym expansion.

And in fact, if you write this code without a standalone kind signature, i.e.,

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where

import Data.Kind (Constraint, Type)

data family Pi t :: Type

type FunctionSymbol :: Type -> Type
type FunctionSymbol t = Type

-- NB: No standalone kind signature
class IsSum (sumf :: FunctionSymbol (p, q)) where
    sumConNames :: Pi (p, q)

And then ask GHCi what the order of type variables is, then it will give exactly the @p @q ordering:

λ> :set -fprint-explicit-kinds 
λ> :info IsSum
type IsSum :: forall p q. FunctionSymbol (p, q) -> Constraint
class IsSum @p @q sumf where
  sumConNames :: Pi (p, q)
  {-# MINIMAL sumConNames #-}
  	-- Defined at Foo.hs:15:1

What's more, GHCi even tells you the kind of IsSum is inferred to be type IsSum :: forall p q. FunctionSymbol (p, q) -> Constraint, exactly as you would expect. This makes it even stranger that it you actually insert this standalone kind signature into the program:

type IsSum :: forall p q. FunctionSymbol (p, q) -> Constraint
class IsSum (sumf :: FunctionSymbol (p, q)) where
    sumConNames :: Pi (p, q)

Then GHC no longer accepts it. So now we have a situation where GHC has no difficulties inferring a type, but it cannot check the type. That seems very smelly.

What about this?

type IsSum :: forall q p. (p,q) -> Constraint
class IsSum (a :: (r,s)) where ...

Today this is accepted. But with your approach (whose attractiveness I can see) the class decl is equivalent to

class IsSum @r @s (a :: (r,s)) where ...

and that doesn't line up with the kind signature. Is that what you expect? Technically this'd be a breaking change, but I doubt anyone will notice!

@rae?

What about this?

type IsWombat :: forall q p. (p,q) -> Constraint
class IsSum (a :: (r,s)) where ...

Ah, that is a very compelling example. Indeed, I don't want to change the behavior of this program, and thinking about how to implement this, it's difficult to see how to implement this other than by unification. And if you use unification, then hiding the type variables behind a type synonym like FunctionSymbol would definitely wreak havoc.

In short, you've won me over to your side. I'm fine with rejecting the original example (even if it is a bit weird that it works without a standalone kind signature).

I'd like to hear from @rae before making a change.

added Pnormal Tbug TypeFamilies compiler crash labels and removed needs triage label

assigned to @rae

mentioned in commit 04cefe37

mentioned in merge request !11579 (closed)

mentioned in commit 713bcdc7

mentioned in commit eb9a8b96

mentioned in commit b00fd698

closed with commit 6dbab180

mentioned in commit 6dbab180

Fixed by

commit 6dbab1808bfbe484b3fb396aab1d105314f918d8
Author: Simon Peyton Jones <simon.peytonjones@gmail.com>
Date:   Tue Nov 7 23:51:19 2023 +0100

    Add an extra check in kcCheckDeclHeader_sig
    
    Fix #24083 by checking for a implicitly-scoped type variable that is not
    actually bound.  See Note [Disconnected type variables] in GHC.Tc.Gen.HsType
    
    For some reason, on aarch64-darwin we saw a 2.8% decrease in compiler
    allocations for MultiLayerModulesTH_Make; but 0.0% on other architectures.
    
    Metric Decrease:
        MultiLayerModulesTH_Make

 compiler/GHC/Tc/Errors/Ppr.hs           | 10 ++++++++++
 compiler/GHC/Tc/Errors/Types.hs         |  7 +++++++
 compiler/GHC/Tc/Gen/HsType.hs           | 66 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++-----
 compiler/GHC/Types/Error/Codes.hs       |  1 +
 compiler/GHC/Types/Hint.hs              |  4 ++++
 compiler/GHC/Types/Hint/Ppr.hs          |  3 +++
 testsuite/tests/polykinds/T24083.hs     | 14 +++++++++++++
 testsuite/tests/polykinds/T24083.stderr |  6 ++++++
 testsuite/tests/polykinds/all.T         |  1 +
 9 files changed, 107 insertions(+), 5 deletions(-)

I'm not sure about backporting. Probably worth it, but it's very much a corner case. Hence re-opening @bgamari @wz1000

reopened

Type checker crash

Child items ...

Activity