Review comments

goldfirere · Sep 5, 2019 · 50c8d06 · 50c8d06
1 parent 886e9cf
commit 50c8d06
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 5 deletions.
diff --git a/src/Data/Singletons/Single/Data.hs b/src/Data/Singletons/Single/Data.hs
@@ -147,7 +147,7 @@ singCtor dataName (DCon con_tvbs cxt name fields rty)
   let indices = map DVarT indexNames
       kindedIndices = zipWith DSigT indices kinds
       args = map (DAppT singFamily) indices
-      kvbs = singTypeKVBs con_tvbs kinds [] rty' []
+      kvbs = singTypeKVBs con_tvbs kinds [] rty' mempty
       all_tvbs = kvbs ++ zipWith DKindedTV indexNames kinds
 
   -- SingI instance for data constructor
@@ -173,3 +173,6 @@ singCtor dataName (DCon con_tvbs cxt name fields rty)
   return $ DCon all_tvbs [] sName conFields
                 (DConT (singTyConName dataName) `DAppT`
                   (foldType pCon indices `DSigT` rty'))
+                  -- Make sure to include an explicit `rty'` kind annotation.
+                  -- See Note [Preserve the order of type variables during singling],
+                  -- wrinkle 3, in D.S.Single.Type.
diff --git a/src/Data/Singletons/Single/Type.hs b/src/Data/Singletons/Single/Type.hs
@@ -41,9 +41,11 @@ singType bound_kvs prom ty = do
   prom_res  <- promoteType_NC res
   let args' = map (\n -> singFamily `DAppT` (DVarT n)) arg_names
       res'  = singFamily `DAppT` (foldl apply prom (map DVarT arg_names) `DSigT` prom_res)
+                -- Make sure to include an explicit `prom_res` kind annotation.
+                -- See Note [Preserve the order of type variables during singling],
+                -- wrinkle 3.
       tau   = ravel args' res'
-      kvbs  = singTypeKVBs orig_tvbs prom_args cxt' prom_res
-                           (map DPlainTV (toList bound_kvs))
+      kvbs     = singTypeKVBs orig_tvbs prom_args cxt' prom_res bound_kvs
       all_tvbs = kvbs ++ zipWith DKindedTV arg_names prom_args
       ty' = DForallT ForallInvis all_tvbs $ DConstrainedT cxt' tau
   return (ty', num_args, arg_names, cxt, prom_args, prom_res)
@@ -58,7 +60,7 @@ singTypeKVBs ::
   -> [DType]      -- ^ The argument types of the signature (promoted).
   -> DCxt         -- ^ The context of the signature (singled).
   -> DType        -- ^ The result type of the signature (promoted).
-  -> [DTyVarBndr] -- ^ The type variables previously bound in the current scope.
+  -> OSet Name    -- ^ The type variables previously bound in the current scope.
   -> [DTyVarBndr] -- ^ The kind variables for the singled type signature.
 singTypeKVBs orig_tvbs prom_args sing_ctxt prom_res bound_tvbs
   | null orig_tvbs
@@ -67,7 +69,7 @@ singTypeKVBs orig_tvbs prom_args sing_ctxt prom_res bound_tvbs
   = deleteFirstsBy
       ((==) `on` extractTvbName)
       (toposortTyVarsOf $ prom_args ++ sing_ctxt ++ [prom_res])
-      bound_tvbs
+      (map DPlainTV $ toList bound_tvbs)
       -- Make sure to subtract out the bound variables currently in scope,
       -- lest we accidentally shadow them in this type signature.
       -- See Note [Explicitly binding kind variables] in D.S.Promote.Monad.