Locally reified class methods don't explicitly quantify kind variables

[RyanGlScott]

If you run the following program:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module Main where

import Language.Haskell.TH
import Language.Haskell.TH.Desugar

main :: IO ()
main = putStrLn
 $([d| class C (f :: k -> Type) where
         method :: forall (a :: k). f a
     |] >>= \ds -> withLocalDeclarations ds (dsReify (mkName "method")) >>= stringE . show)

You'll get the following type for method:

$ /opt/ghc/8.4.3/bin/runghc Bug2.hs
Just (DVarI method (DForallT [DKindedTV f_6989586621679035180 (DAppT (DAppT DArrowT (DVarT k_6989586621679035179)) (DConT Language.Haskell.TH.Syntax.Type))] [DAppPr (DConPr C_6989586621679035177) (DVarT f_6989586621679035180)] (DForallT [DKindedTV a_6989586621679035181 (DVarT k_6989586621679035179)] [] (DAppT (DVarT f_6989586621679035180) (DVarT a_6989586621679035181)))) (Just C_6989586621679035177))

After some cleanup, that's:

method :: forall (f :: k -> Type). C f => forall (a :: k). f a

This type isn't wrong today, but once ghc-proposals/ghc-proposals#103 is implemented, this will be incorrect, since k is implicitly brought into scope in a top-level forall.

[RyanGlScott]

If we do fix this, we should be careful to see how singletons reacts, since it turns out to be very sensitive to the number of type variable binders that a reified class method's type signature contains at the beginning.

[RyanGlScott]

A similar problem exists for data constructors:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
module Main where

import Data.Proxy
import Language.Haskell.TH hiding (Type)
import Language.Haskell.TH.Desugar

main :: IO ()
main = print
 $([d| data D (a :: k) = MkD { unD :: Proxy a }
     |] >>= \ds -> do
     withLocalDeclarations ds (dsReify (mkName "MkD")) >>= runIO . print . show
     withLocalDeclarations ds (dsReify (mkName "unD")) >>= runIO . print . show
     [| () |])

$ /opt/ghc/8.6.1/bin/runghc Bug.hs
"Just (DVarI MkD (DForallT [DPlainTV a_6989586621679037317] [] (DAppT (DAppT DArrowT (DAppT (DConT Data.Proxy.Proxy) (DVarT a_6989586621679037317))) (DAppT (DConT D_6989586621679037313) (DVarT a_6989586621679037317)))) (Just D_6989586621679037313))"
-- Cleaned up: MkD :: forall a. Proxy a -> D a
"Just (DVarI unD (DForallT [DPlainTV a_6989586621679037317] [] (DAppT (DAppT DArrowT (DAppT (DConT D_6989586621679037313) (DVarT a_6989586621679037317))) (DAppT (DConT Data.Proxy.Proxy) (DVarT a_6989586621679037317)))) Nothing)"
-- Cleaned up: unD :: forall a. D a -> Proxy a 
()

This time, the kind k is simply dropped altogether.

[RyanGlScott]

One reason for the kind-dropping in #88 (comment) is because of the definition of tvbToType, which drops kinds from KindedTVs:

th-desugar/Language/Haskell/TH/Desugar/Util.hs

Lines 115 to 117 in cb8092f

	-- | Convert a 'TyVarBndr' into a 'Type'
	tvbToType :: TyVarBndr -> Type
	tvbToType = VarT . tvbName

Yikes. Thankfully, tvbToType is only used internally, so we can change it to preserve kind information without remorse:

diff --git a/Language/Haskell/TH/Desugar/Util.hs b/Language/Haskell/TH/Desugar/Util.hs
index 2fe6283..5106805 100644
--- a/Language/Haskell/TH/Desugar/Util.hs
+++ b/Language/Haskell/TH/Desugar/Util.hs
@@ -114,7 +114,8 @@ tvbName (KindedTV n _) = n
 
 -- | Convert a 'TyVarBndr' into a 'Type'
 tvbToType :: TyVarBndr -> Type
-tvbToType = VarT . tvbName
+tvbToType (PlainTV n)    = VarT n
+tvbToType (KindedTV n k) = SigT (VarT n) k
 
 -- | Do two names name the same thing?
 nameMatches :: Name -> Name -> Bool

That makes the results a little more palatable:

"Just (DVarI MkD (DForallT [DPlainTV k_6989586621679157832,DPlainTV a_6989586621679157833] [] (DAppT (DAppT DArrowT (DAppT (DConT Data.Proxy.Proxy) (DVarT a_6989586621679157833))) (DAppT (DConT D_6989586621679157829) (DSigT (DVarT a_6989586621679157833) (DVarT k_6989586621679157832))))) (Just D_6989586621679157829))"
-- Cleaned up: MkD :: forall k a. Proxy a -> D (a :: k)
"Just (DVarI unD (DForallT [DPlainTV k_6989586621679157832,DPlainTV a_6989586621679157833] [] (DAppT (DAppT DArrowT (DAppT (DConT D_6989586621679157829) (DSigT (DVarT a_6989586621679157833) (DVarT k_6989586621679157832)))) (DAppT (DConT Data.Proxy.Proxy) (DVarT a_6989586621679157833)))) Nothing)"
-- Cleaned up: unD :: forall k a. D (a :: k) -> Proxy a

It's still a little unsatisfying, though, since we'd ideally have forall k (a :: k). .... In fact, it starts out that way, but we drop the k from (a :: k) in this line of code:

th-desugar/Language/Haskell/TH/Desugar/Reify.hs

Line 357 in cb8092f

tvbs = map PlainTV $ S.elems $ freeNamesOfTypes ty_args

In order to preserve the telescope, we'd need an equivalent of toposortTyVarsOf for Types.

[RyanGlScott]

Thankfully, the th-abstraction library will be gaining such a toposortTyVarsOf counterpart for Types in its next release. Perhaps we could just add a dependency on th-abstraction and use that?