search

goldfirere / singletons

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

`singletons-th`: Make `pr_scoped_vars` a list of `LocalVar`s, not `Name`s #614

Closed RyanGlScott closed 4 months ago

RyanGlScott commented 4 months ago

Doing so makes it possible to track the kinds of scoped type variables with greater precision during lambda lifting. See the golden output for the new T613 test case to see an example of this in action.

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

RyanGlScott commented 4 months ago

This PR has revealed a latent bug. Consider this variation on the T613 test case:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Bug where

import Data.Proxy
import Data.Proxy.Singletons
import Data.Singletons.TH

$(promote [d|
  f :: forall k (a :: k). Proxy a -> Proxy a
  f = g
    where
      g :: forall (b :: k). Proxy b -> Proxy b
      g x = y
        where
          y = Proxy
  |])

After the changes in this PR, this program now fails to promote:

$ ghc-9.10 Bug.hs 
Loaded package environment from /home/ryanglscott/Documents/Hacking/Haskell/ci-maintenance/checkout/goldfirere/singletons/.ghc.environment.x86_64-linux-9.10.1
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
Bug.hs:(13,2)-(21,5): Splicing declarations
    promote
      [d| f_a48w ::
            forall k_a48x (a_a48y :: k_a48x). Proxy a_a48y -> Proxy a_a48y
          f_a48w
            = g_a4ac
            where
                g_a4ac :: forall (b_a4ad :: k_a48x). Proxy b_a4ad -> Proxy b_a4ad
                g_a4ac x_a4ae
                  = y_a4af
                  where
                      y_a4af = Proxy |]
  ======>
    f_a4kr ::
      forall k_a4kp (a_a4kq :: k_a4kp). Proxy a_a4kq -> Proxy a_a4kq
    f_a4kr
      = g_a4kt
      where
          g_a4kt :: forall (b_a4ks :: k_a4kp). Proxy b_a4ks -> Proxy b_a4ks
          g_a4kt x_a4ku
            = y_a4kv
            where
                y_a4kv = Proxy
    type family Let6989586621679026486YSym0 (b6989586621679026436 :: k6989586621679026433) k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (x6989586621679026485 :: Proxy b6989586621679026436) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) where
      Let6989586621679026486YSym0 b6989586621679026436 k6989586621679026433 a6989586621679026434 x6989586621679026485 a_69895866216790264766989586621679026481 = Let6989586621679026486Y b6989586621679026436 k6989586621679026433 a6989586621679026434 x6989586621679026485 a_69895866216790264766989586621679026481
    type family Let6989586621679026486Y (b6989586621679026436 :: k6989586621679026433) k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (x6989586621679026485 :: Proxy b6989586621679026436) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) where
      Let6989586621679026486Y b_a4ks k_a4kp a_a4kq x_a4lf a_6989586621679026476_a4lb = ProxySym0
    data Let6989586621679026482GSym0 k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) :: (~>) (Proxy b6989586621679026436) (Proxy b6989586621679026436)
      where
        Let6989586621679026482GSym0KindInference :: SameKind (Apply (Let6989586621679026482GSym0 k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481) arg_a4le) (Let6989586621679026482GSym1 k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481 arg_a4le) =>
                                                    Let6989586621679026482GSym0 k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481 a6989586621679026483
    type instance Apply @(Proxy b6989586621679026436) @(Proxy b6989586621679026436) (Let6989586621679026482GSym0 k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481) a6989586621679026483 = Let6989586621679026482G k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481 a6989586621679026483
    instance SuppressUnusedWarnings (Let6989586621679026482GSym0 k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481) where
      suppressUnusedWarnings
        = snd ((,) Let6989586621679026482GSym0KindInference ())
    type family Let6989586621679026482GSym1 k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) (a6989586621679026483 :: Proxy b6989586621679026436) :: Proxy b6989586621679026436 where
      Let6989586621679026482GSym1 k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481 a6989586621679026483 = Let6989586621679026482G k6989586621679026433 a6989586621679026434 a_69895866216790264766989586621679026481 a6989586621679026483
    type family Let6989586621679026482G k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) (a_a4ld :: Proxy b_a4ks) :: Proxy b_a4ks where
      Let6989586621679026482G k_a4kp a_a4kq a_6989586621679026476_a4lb (x_a4lf :: Proxy b_a4ks) = Let6989586621679026486YSym0 b_a4ks k_a4kp a_a4kq x_a4lf a_6989586621679026476_a4lb
    type FSym0 :: forall k_a4kp
                         (a_a4kq :: k_a4kp). (~>) (Proxy a_a4kq) (Proxy a_a4kq)
    data FSym0 :: (~>) (Proxy a_a4kq) (Proxy a_a4kq)
      where
        FSym0KindInference :: SameKind (Apply FSym0 arg_a4l9) (FSym1 arg_a4l9) =>
                              FSym0 a6989586621679026480
    type instance Apply @(Proxy a_a4kq) @(Proxy a_a4kq) FSym0 a6989586621679026480 = F a6989586621679026480
    instance SuppressUnusedWarnings FSym0 where
      suppressUnusedWarnings = snd ((,) FSym0KindInference ())
    type FSym1 :: forall k_a4kp (a_a4kq :: k_a4kp). Proxy a_a4kq
                                                    -> Proxy a_a4kq
    type family FSym1 @k_a4kp @(a_a4kq :: k_a4kp) (a6989586621679026480 :: Proxy a_a4kq) :: Proxy a_a4kq where
      FSym1 a6989586621679026480 = F a6989586621679026480
    type F :: forall k_a4kp (a_a4kq :: k_a4kp). Proxy a_a4kq
                                                -> Proxy a_a4kq
    type family F @k_a4kp @(a_a4kq :: k_a4kp) (a_a4l8 :: Proxy a_a4kq) :: Proxy a_a4kq where
      F @k_a4kp @a_a4kq (a_6989586621679026476_a4lb :: Proxy a_a4kq) = Apply (Let6989586621679026482GSym0 k_a4kp a_a4kq a_6989586621679026476_a4lb) a_6989586621679026476_a4lb
Bug.hs:13:2: error: [GHC-76037]
    Not in scope: type variable ‘k6989586621679026433’
   |
13 | $(promote [d|
   |  ^^^^^^^^^^^^...

Bug.hs:13:2: error: [GHC-76037]
    Not in scope: type variable ‘k6989586621679026433’
   |
13 | $(promote [d|
   |  ^^^^^^^^^^^^...

Note the generated code for Let6989586621679026486Y:

    type family Let6989586621679026486Y (b6989586621679026436 :: k6989586621679026433) k6989586621679026433 (a6989586621679026434 :: k6989586621679026433) (x6989586621679026485 :: Proxy b6989586621679026436) (a_69895866216790264766989586621679026481 :: Proxy a6989586621679026434) where
      Let6989586621679026486Y b_a4ks k_a4kp a_a4kq x_a4lf a_6989586621679026476_a4lb = ProxySym0

This quantifies b6989586621679026436 :: k6989586621679026433 before it quantifies k6989586621679026433, which is ill-scoped. The reason for this out-of-order quantification is this code:

https://github.com/goldfirere/singletons/blob/9d5a8119425c58e667fc2d88d8db0a0013355240/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs#L82-L88

Note that the newly bound scoped type variables are placed before type variables that were bound earlier, resulting in oddities like the ones seen above. This wasn't as much of a problem back when we didn't track the kinds of scoped type variables, but now that we do, it's a much more glaring issue.

We should swap the order of binds and scoped.

RyanGlScott commented 4 months ago

We should swap the order of binds and scoped.

...at least, I thought that would fix the issue above. Sadly, doing that just reveals another issue, this time with Let6989586621679026606G:

    type family Let6989586621679026606G k6989586621679026557 (a6989586621679026558 :: k6989586621679026557) (a_69895866216790266006989586621679026605 :: Proxy a6989586621679026558) (a_a4nd :: Proxy b_a4ms) :: Proxy b_a4ms where
      Let6989586621679026606G k_a4mp a_a4mq a_6989586621679026600_a4nb (x_a4nf :: Proxy b_a4ms) = Let6989586621679026610YSym0 k_a4mp a_a4mq b_a4ms a_6989586621679026600_a4nb x_a4nf

<snip>

Bug.hs:13:2: error: [GHC-87279]
    • The kind of ‘Let6989586621679026606G’ is ill-scoped
        Inferred kind: Let6989586621679026606G :: forall (b :: k6989586621679026557).
                                                  forall k6989586621679026557
                                                         (a6989586621679026558 :: k6989586621679026557) ->
                                                  Proxy a6989586621679026558 -> Proxy b -> Proxy b
      NB: Specified variables
        (namely: (b :: k6989586621679026557)) always come first
      Perhaps try this order instead:
        k6989586621679026557
        (b :: k6989586621679026557)
        (a6989586621679026558 :: k6989586621679026557)
        (a_69895866216790266006989586621679026605 :: Proxy
                                                       a6989586621679026558)
        (a :: Proxy b)
    • In the type family declaration for ‘Let6989586621679026606G’
   |
13 | $(promote [d|
   |  ^^^^^^^^^^^^...

It's not obvious to me how we'd make this work without giving Let6989586621679026606G a standalone kind signature, but we don't give standalone kind signatures to local definitions for the reasons described in this Note. In light of this, perhaps we just can't support examples like the one above for now.