[Failing] try to get rid of Proxy in signature of withRegion

examples-version-changes/ghc-dps-compact/after/Compact/BFTraversal.hs

@@ -14,6 +14,7 @@
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE UnicodeSyntax #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
 {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}
 
@@ -84,7 +85,7 @@ mapPhasesBFS f = runPhases NonLin.. bft' f
 mapAccumBFS :: forall a b s. (s -> a -> (s, b)) -> s -> BinTree a -> (BinTree b, s)
 mapAccumBFS f s0 tree =
   unur . withRegion $
-    \(_ :: Proxy r) token ->
+    \ @r token ->
       fromIncomplete $
         alloc @r token
           <&> \dtree -> go s0 (singletonN (Ur tree, dtree))

examples-version-changes/ghc-dps-compact/after/Compact/DList.hs

@@ -9,14 +9,14 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# OPTIONS_GHC -Wno-name-shadowing -Wno-type-defaults #-}
 {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}
 
 module Compact.DList where
 
 import Compact.Destination
 import Control.Functor.Linear ((<&>))
-import Data.Proxy (Proxy)
 import Prelude.Linear hiding (concat, foldl', foldr)
 
 newtype DList r a = DList (Incomplete r [a] (Dest r [a]))
@@ -93,7 +93,7 @@ differenceListDestLeft :: [[a]] -> [a]
 differenceListDestLeft lists =
   unur
     ( withRegion
-        ( \(_ :: Proxy r) t ->
+        ( \ @r t ->
             let f :: (Token, DList r a) %1 -> [a] -> (Token, DList r a)
                 f (t, dl) ys =
                   let !(t', t'') = dup2 t

examples-version-changes/ghc-dps-compact/after/Compact/Map.hs

@@ -10,6 +10,7 @@
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# OPTIONS_GHC -Wno-name-shadowing -Wno-type-defaults #-}
 {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}
 
@@ -18,7 +19,6 @@ module Compact.Map where
 import Compact.Destination
 import Control.Functor.Linear ((<&>))
 import Data.Kind (Type)
-import Data.Proxy (Proxy)
 import Prelude.Linear
 
 mapL :: forall a b. (a %1 -> b) -> [a] -> [b]
@@ -129,7 +129,7 @@ mapDestFS f l dl =
 -------------------------------------------------------------------------------
 
 dpsWrapper :: (forall (r :: Type) a b. (Region r) => (a %1 -> b) -> [a] -> Dest r [b] %1 -> ()) -> (Int %1 -> Int) -> [Int] -> [Int]
-dpsWrapper impl f l = unur (withRegion (\(_ :: Proxy r) t -> fromIncomplete_ (alloc @r t <&> \d -> impl f l d)))
+dpsWrapper impl f l = unur (withRegion (\ @r t -> fromIncomplete_ (alloc @r t <&> \d -> impl f l d)))
 
 impls' :: (Int %1 -> Int) -> [([Int] -> [Int], String, Bool)]
 impls' f =

examples-version-changes/ghc-dps-compact/after/Compact/Queue.hs

@@ -9,6 +9,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# OPTIONS_GHC -Wno-name-shadowing -Wno-type-defaults #-}
 {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}
 
@@ -17,7 +18,6 @@ module Compact.Queue where
 import Compact.DList
 import qualified Compact.DList as DList
 import Compact.Destination
-import Data.Proxy (Proxy)
 import Data.Word
 import Prelude.Linear hiding ((*), (+), (<))
 import Prelude ((*), (+), (<))
@@ -114,7 +114,7 @@ funcImpl limit = go 0 (singletonF 1)
               else q'
 
 destImpl :: Word64 -> Word64
-destImpl limit = unur (withRegion (\(_ :: Proxy r) t -> let r = go 0 (singleton @r t (Ur 1)) in move r))
+destImpl limit = unur (withRegion (\ @r t -> let r = go 0 (singleton @r t (Ur 1)) in move r))
   where
     go :: (Region r) => Word64 -> Queue r (Ur Word64) %1 -> Word64
     go sum q = case dequeue q of

examples-version-changes/ghc-dps-compact/after/Compact/SExpr.hs

@@ -11,6 +11,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeAbstractions #-}
 {-# OPTIONS_GHC -Wno-name-shadowing #-}
 {-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-all #-}
 
@@ -212,7 +213,7 @@ parseWithoutDest bs = case parseWithoutDest' bs 0 of
 parseWithDest :: ByteString -> Either SExprParseError SExpr
 parseWithDest bs =
   let Ur (sexpr, res) =
-        withRegion $ \(_ :: Proxy r) token ->
+        withRegion $ \ @r token ->
           fromIncomplete $
             alloc @r token
               <&> \d ->

src-version-changes/ghc-dps-compact/after/Compact/Destination/Internal.hs

@@ -172,11 +172,11 @@ getRegionInfo :: forall r. (Region r) => RegionInfo
 getRegionInfo = reflect (Proxy :: Proxy r)
 {-# INLINE getRegionInfo #-}
 
-withRegion :: forall b. (forall (r :: Type). (Region r) => Proxy r -> Token %1 -> Ur b) %1 -> Ur b
+withRegion :: forall b. (forall (r :: Type). (Region r) => Token %1 -> Ur b) %1 -> Ur b
 withRegion = toLinear _withRegion
 {-# INLINE withRegion #-}
 
-_withRegion :: forall b. (forall (r :: Type). (Region r) => Proxy r -> Token %1 -> Ur b) -> Ur b
+_withRegion :: forall b. (forall (r :: Type). (Region r) => Token %1 -> Ur b) -> Ur b
 _withRegion f =
   unsafePerformIO $ do
     c <- (compact firstInhabitant)
@@ -185,7 +185,7 @@ _withRegion f =
     putDebugLn $
       "withRegion: allocating new region around @"
         ++ (show firstPtr)
-    let !result = reify (RegionInfo c) (\(proxy :: Proxy s) -> f @s proxy Token)
+    let !result = reify (RegionInfo c) (\(_ :: Proxy s) -> f @s Token)
     resultPtr <- IO (\s -> case anyToAddr# result s of (# s', addr# #) -> (# s', W# (addr2Word# addr#) #))
     putDebugLn $
       "withRegion: exiting and returning @"

test-version-changes/ghc-dps-compact/after/Test/Compact/Destination.hs

@@ -12,6 +12,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE TypeAbstractions #-}
 
 module Test.Compact.Destination (destinationTests) where
 
@@ -39,7 +40,7 @@ data Foo a b = MkFoo {unBar :: a, unBaz :: (b, b), unBoo :: a} deriving (Eq, Gen
 compOnFreshAlloc :: IO String
 compOnFreshAlloc = do
   let actual :: Ur (Int, Int)
-      !actual = withRegion $ \(_ :: Proxy r) t -> case dup2 t of
+      !actual = withRegion $ \ @r t -> case dup2 t of
         (t', t'') ->
           fromIncomplete_ $
             (alloc @r t')
@@ -60,7 +61,7 @@ compOnFreshAlloc = do
 compOnUsedAlloc :: IO String
 compOnUsedAlloc = do
   let actual :: Ur (Int, (Int, Int))
-      !actual = withRegion $ \(_ :: Proxy r) t -> case dup2 t of
+      !actual = withRegion $ \ @r t -> case dup2 t of
         (t', t'') ->
           fromIncomplete_ $
             (alloc @r t')
@@ -81,7 +82,7 @@ compOnUsedAlloc = do
 fillCustomDataAndExtract :: IO String
 fillCustomDataAndExtract = do
   let actual :: Ur (Foo Int Char, Int)
-      !actual = withRegion $ \(_ :: Proxy r) t ->
+      !actual = withRegion $ \ @r t ->
         fromIncomplete $
           (alloc @r t)
             <&> ( \d ->