goldfirere / singletons

Fake dependent types in Haskell using singletons
287 stars 36 forks source link

Require building with GHC 9.10 #587

Closed RyanGlScott closed 6 months ago

RyanGlScott commented 6 months ago

This is a collection of patches needed to make singletons, singletons-th, and singletons-base build with GHC 9.10 (and in the case of singletons-{th,base}, require them to build with GHC 9.10). The two most interesting commits (whose commit messages I have included below) are the ones involving changes to the arities of type families. GHC 9.10 no longer performs arity inference (see the commit messages below), so we need to explicitly use TypeAbstractions in more places to give promoted type families the correct arities.

This makes more progress towards https://github.com/goldfirere/singletons/issues/569.

singletons: Support building with GHC 9.10

Because GHC 9.10 no longer performs arity inference in type-level declarations (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst), we now must use TypeAbstractions in certain singletons definitions to make GHC 9.10 accept them.

One part of a fix for https://github.com/goldfirere/singletons/issues/566.

singletons-th: Adapt to GHC 9.10's lack of arity inference

GHC 9.10 no longer performs arity inference in type-level declarations (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst), and as it turns out, many of the promoted type families that singletons-th generates would have the wrong arity. For instance, singletons-th would promote this definition:

f :: Either a Bool
f = Right True

To this type family:

type F :: Either a Bool
type family F where
  F = Right True

With GHC 9.10 or later, however, GHC would conclude that F has arity 0, which means that it should not bind any arguments (visible or invisible). The type family equation for F, however, only works if F has arity 1! This is because the type family equation needs to bind an invisible @a argument:

  F @A = Right @A @Bool True

To ensure that type families like F have the expected arity, singletons-th now uses TypeAbstractions in more places to ensure that type family headers bind an appropriate number of type variables, which makes the type families' arities explicit. For instance, singletons-th now generates the following code for F:

type F :: Either a Bool
type family F @A where -- Note the @A here, which gives it arity 1
  F = Right True

For more details on how this is implemented, see the new Note [Generating type families with the correct arity] in Data.Singletons.TH.Promote.

A consequence of this change is that the average piece of singletons-th–generated code is much more likely to require TypeAbstractions than it did before. This explains why we now enable TypeAbstractions in almost every module in singletons-base.

Fixes https://github.com/goldfirere/singletons/issues/566.