Skip to content

Commit

Permalink
Record local variables' kinds during lambda lifting
Browse files Browse the repository at this point in the history
Previously, `singletons-th` made no effort to track the kinds of local
variables when generating lambda-lifted code, instead generating local variable
binders with no kind annotations. As a result, GHC would generalize the kinds
of these lambda-lifted definitions to things that are way more polymorphic than
intended. While this technically works in today's GHC, it won't in a future
version of GHC that implements
[GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515).

In general, generating kinds for every local variable would require
`singletons-th` to implement something akin to full-blown type inference over
the Template Haskell AST, which is not something I am eager to implement.

Fortunately, there is a relatively simple approach we can do to alleviate this
problem that doesn't require full type inference. In situations where we know
the kind of a local variable (e.g., when there is a top-level signature or
there is a pattern signature), we record the variable's kind and use it when
generating binders for any lambda-lifted definitions that close over the
variable. For the full story on how this works, see `Note [Local variables and
kind information]` `D.S.TH.Promote.Syntax.LocalVar`.

This is not a perfect solution, as there will still be examples of the original
problem that won't be covered by this simple approach (see the Note). This
approach is still much better than what `singletons-th` was doing before, and I
think it's worth using this simple approach even if it doesn't fix 100% of all
cases.

This patch mostly resolves the "Overly polymorphic lambda-lifting, part 2"
section of #601.
  • Loading branch information
RyanGlScott committed Jun 30, 2024
1 parent b385b36 commit 58dba67
Show file tree
Hide file tree
Showing 36 changed files with 646 additions and 373 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -354,18 +354,18 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
type SchSym1 :: [Attribute] -> Schema
type family SchSym1 (a0123456789876543210 :: [Attribute]) :: Schema where
SchSym1 a0123456789876543210 = Sch a0123456789876543210
type family LamCases_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 (name0123456789876543210 :: [AChar]) name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 name name' u attrs 'True = u
LamCases_0123456789876543210 name name' u attrs 'False = Apply (Apply LookupSym0 name) (Apply SchSym0 attrs)
data LamCases_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 (name0123456789876543210 :: [AChar]) name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210) arg) (LamCases_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 (name0123456789876543210 :: [AChar]) name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 a_01234567898765432100123456789876543210
type LookupSym0 :: (~>) [AChar] ((~>) Schema U)
data LookupSym0 :: (~>) [AChar] ((~>) Schema U)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -62,18 +62,18 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
insertionSort :: [Nat] -> [Nat]
insertionSort [] = []
insertionSort (h : t) = insert h (insertionSort t)
type family LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 (n0123456789876543210 :: Nat) h0123456789876543210 t0123456789876543210 a_0123456789876543210 where
LamCases_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
LamCases_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
data LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 (n0123456789876543210 :: Nat) h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) arg) (LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 (n0123456789876543210 :: Nat) h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 a_01234567898765432100123456789876543210
type InsertionSortSym0 :: (~>) [Nat] [Nat]
data InsertionSortSym0 :: (~>) [Nat] [Nat]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -37,82 +37,82 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations
in z
foo5 :: a -> a
foo5 x = case x of y -> (\ _ -> x) y
type family LamCases_0123456789876543210 y0123456789876543210 x0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 y x _ = x
data LamCases_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 y0123456789876543210 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 y0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 y0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 y0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 y0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 x0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 x y = Apply (LamCases_0123456789876543210Sym0 y x) y
data LamCases_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type family Let0123456789876543210ZSym0 a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
type family Let0123456789876543210ZSym0 a0123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where
Let0123456789876543210ZSym0 a0123456789876543210 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210
type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where
type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where
Let0123456789876543210Z a y x = y
type family LamCases_0123456789876543210 a0123456789876543210 x0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 a x y = Let0123456789876543210ZSym0 a y x
data LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 a0123456789876543210 b0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 a b '(p, _) = p
data LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) arg) (LamCases_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 d0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 d ('Just y) = y
data LamCases_0123456789876543210Sym0 d0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 (d0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 d0123456789876543210) arg) (LamCases_0123456789876543210Sym1 d0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 d0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 d0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 d0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 d0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 d0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 (d0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 d0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 d0123456789876543210 a_01234567898765432100123456789876543210
type family LamCases_0123456789876543210 d0123456789876543210 x0123456789876543210 a_0123456789876543210 where
type family LamCases_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) a_0123456789876543210 where
LamCases_0123456789876543210 d x ('Just y) = y
LamCases_0123456789876543210 d x 'Nothing = d
data LamCases_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
data LamCases_0123456789876543210Sym0 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) a_01234567898765432100123456789876543210
where
LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 d0123456789876543210 x0123456789876543210 arg) =>
LamCases_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 d0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210) where
suppressUnusedWarnings
= snd ((,) LamCases_0123456789876543210Sym0KindInference ())
type family LamCases_0123456789876543210Sym1 d0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 where
type family LamCases_0123456789876543210Sym1 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) a_01234567898765432100123456789876543210 where
LamCases_0123456789876543210Sym1 d0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 d0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
type Foo5Sym0 :: (~>) a a
data Foo5Sym0 :: (~>) a a
Expand Down
Loading

0 comments on commit 58dba67

Please sign in to comment.