GHC+DH Weekly Update #7, 2023-06-14

#1

This week Vlad and I created individual tickets for all remaining parts of GHC Proposal #425 “Invisible binders in type declarations”:

  • #23501 “Wildcard binders in type declarations”
  • #23502 “Kind inference for invisible binders in type declarations”
  • #23515 “Type/data instances: require that the instantiation is determined by the LHS alone”
  • #23512 “Type/data instances: require that variables on the RHS are mentioned on the LHS”
  • #23510 “Implement the -Wimplicit-rhs-quantification warning”
  • #23514 “Remove arity inference in type declarations”

And immediately began to solve them resulting in the following merge requests:

  • !10644 “Type/data instances: require that variables on the RHS are mentioned on the LHS”
  • !10638 “Implement the -Wimplicit-rhs-quantification warning”
  • !10660 “Remove arity inference in type declarations”

One of those issues turned out to be more difficult to solve because it involves modifying the type checker (#23515). I’m currently in the process of debugging a compiler crash caused by my changes

No skolem info - we could not find the origin of the following variables
  [(UnkSkol (please report this as a bug)
    Call stack:
        CallStack (from HasCallStack):
          unkSkolAnon, called at compiler/GHC/Tc/Types/Origin.hs:315:42 in ghc-9.7-inplace:GHC.Tc.Types.Origin
          unkSkol, called at compiler/GHC/Tc/Utils/TcType.hs:583:31 in ghc-9.7-inplace:GHC.Tc.Utils.TcType
          vanillaSkolemTvUnk, called at compiler/GHC/Types/Var.hs:1094:56 in ghc-9.7-inplace:GHC.Types.Var,
    [k3])]
This should not happen, please report it as a bug following the instructions at:
https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug

Here is a summary of the changes implemented in the submitted merge requests:

  1. Type synonym definitions that rely on outermost kind signatures to bring variables into scope must be rewritten with @k-binders:

    type T1 :: forall a . Maybe a
type T1    = 'Nothing :: Maybe a      -- old
type T1 @a = 'Nothing :: Maybe a      -- new

    To help users identify the code that needs to change a new warning was implemented: -Wimplicit-rhs-quantification

  2. Type and data family instances that rely on outermost kind signatures to bring variables into scope now require either an explicit forall or mentioning the variables on the left-hand side.

    The following example is now rejected with an out-of-scope error:

    type family F1 a :: k
type instance F1 Int = Any :: j -> j

    T23512a.hs:6:31: error: [GHC-76037] Not in scope: type variable ‘j’
T23512a.hs:6:36: error: [GHC-76037] Not in scope: type variable ‘j’

    And here are the ways to fix it:

    type family F2 a :: k
type instance F2 @(j -> j) Int = Any :: j -> j

type family F3 a :: k
type instance forall j. F3 Int = Any :: j -> j

    Notably those are not @k-binders, but ordinary type applications, so you don’t have to wait for 9.8 to fix such code. Because of this there is no warning.

  3. The subtle and fragile arity inference algorithm was removed. Now GHC infers the smallest possible arity making examples like this possible:

    data T (f :: forall r . (TYPE r) -> Type) = MkT (f Int) (f Int#)

tcodeq :: T CodeQ
tcodeq = MkT [||5||] [||5#||]

    GHC used to reject this because it assigned arity = 1 to CodeQ based on its definition:

    type CodeQ :: TYPE r -> Kind.Type
type CodeQ = Code Q

    The new simple approach assigns arity = 0 to this type synonym. But it also means that the following code is now rejected:

    type F :: Type -> forall k. Maybe k
type family F x where
  F Int @Type = Just Bool
  F Int       = Just Either

    It can be fixed using @k-binders:

    type family F x @k where

Finally, my fix for -Wterm-variable-capture was reviewed by Ryan (thank you!) and merged in commit b84a2900.

This work is funded by Serokell

9 Likes
#2

This week I attended ZuriHac and the colocated GHC Workshop, where I had the opportunity to discuss some tricky design issues with other GHC developers.

This resulted in the following proposal amendment to StandaloneKindSignatures that aims to reconcile them with ExtendedForAllScope:

  • #592 “Scoped kind variables in standalone kind signatures”

The discussion of #22762 “eqType, tcEqType, and foralls” led us to the conclusion that we probably want visibility coercions in Core. A prototype implementation of this idea by Matthew Craven can be found at !10331 “Track visibility in forall-coercions”.

It also turned out that there is a subtle bug that led GHC to unify forall a. t with forall a -> t if it was hidden underneath another forall:

type D :: forall j -> forall i.   (i -> j) -> Type
data D :: forall j -> forall i -> (i -> j) -> Type
                        --     ^^^
                        --  incorrectly accepted despite different forall visibility flags

I submitted a fix for this in !10656 "Check visibility of nested foralls in can_eq_nc".

Finally, here’s a fun little story about explicit imports. While working on one of the tickets, I was faced with the following error message:

Expected a type, but found something with kind ‘Type’

It took me a disproportionally long amount of time figure it out, but it turned out that the Type that was in scope simply came from Language.Haskell.TH.Syntax instead of Data.Kind. As soon as I fixed this with a qualified import, I was able to add standalone kind signatures to Code and TExp in commit a0c27cee2394.

6 Likes