dMatchUpSAKWithDecl: Fix treatment of invisible foralls without corre…

…sponding @-binders

After this patch, `dMatchUpSAKWithDecl` is now able to handle a standalone kind
signature with an invisible `forall` without a corresponding `@`-binder, as
seen in the example below:

```hs
type D :: forall (a :: Type). Type
data D
```

While I was in town, I did some code cleanup in `dMatchUpSAKWithDecl` to make
sure that all of the various error conditions are checked more thoroughly,
documenting what parts of the code rely on which preconditions more precisely.
I also applied the same treatment to `matchUpSAKWithDecl`.

Fixes #228.

Language/Haskell/TH/Desugar/Core.hs

@@ -2154,7 +2154,7 @@ dMatchUpSigWithDecl = go_fun_args M.empty
       -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag]
     go_fun_args _ DFANil [] =
       pure []
-    -- This should not happen, per the function's precondition
+    -- This should not happen, per precondition (1).
     go_fun_args _ DFANil decl_bndrs =
       fail $ "dMatchUpSigWithDecl.go_fun_args: Too many binders: " ++ show decl_bndrs
     -- GHC now disallows kind-level constraints, per this GHC proposal:
@@ -2170,51 +2170,66 @@ dMatchUpSigWithDecl = go_fun_args M.empty
       go_invis_tvbs subst tvbs sig_args decl_bndrs
     go_fun_args subst (DFAForalls (DForallVis tvbs) sig_args) decl_bndrs =
       go_vis_tvbs subst tvbs sig_args decl_bndrs
-    go_fun_args subst (DFAAnon anon sig_args) (decl_bndr:decl_bndrs) = do
-      let decl_bndr_name = dtvbName decl_bndr
-          mb_decl_bndr_kind = extractTvbKind decl_bndr
-          anon' = SC.substTy subst anon
-
-          anon'' =
-            case mb_decl_bndr_kind of
-              Nothing -> anon'
-              Just decl_bndr_kind ->
-                let mb_match_subst = matchTy NoIgnore decl_bndr_kind anon' in
-                maybe decl_bndr_kind (`SC.substTy` decl_bndr_kind) mb_match_subst
-      sig_args' <- go_fun_args subst sig_args decl_bndrs
-      pure $ DKindedTV decl_bndr_name Required anon'' : sig_args'
+    go_fun_args subst (DFAAnon anon sig_args) (decl_bndr:decl_bndrs) =
+      case dtvbFlag decl_bndr of
+        -- If the next decl_bndr is required, then we must match its kind (if
+        -- one is provided) against the anonymous kind argument.
+        BndrReq -> do
+          let decl_bndr_name = dtvbName decl_bndr
+              mb_decl_bndr_kind = extractTvbKind decl_bndr
+              anon' = SC.substTy subst anon
+
+              anon'' =
+                case mb_decl_bndr_kind of
+                  Nothing -> anon'
+                  Just decl_bndr_kind ->
+                    let mb_match_subst = matchTy NoIgnore decl_bndr_kind anon' in
+                    maybe decl_bndr_kind (`SC.substTy` decl_bndr_kind) mb_match_subst
+          sig_args' <- go_fun_args subst sig_args decl_bndrs
+          pure $ DKindedTV decl_bndr_name Required anon'' : sig_args'
+        -- We have a visible, anonymous argument in the kind, but an invisible
+        -- @-binder as the next decl_bndr. This is ill kinded, so throw an
+        -- error.
+        --
+        -- This should not happen, per precondition (2).
+        BndrInvis ->
+          fail $ "dMatchUpSigWithDecl.go_fun_args: Expected visible binder, encountered invisible binder: "
+              ++ show decl_bndr
     -- This should not happen, per precondition (1).
     go_fun_args _ _ [] =
       fail "dMatchUpSigWithDecl.go_fun_args: Too few binders"
 
     go_invis_tvbs :: DSubst -> [DTyVarBndrSpec] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag]
     go_invis_tvbs subst [] sig_args decl_bndrs =
       go_fun_args subst sig_args decl_bndrs
-    -- This should not happen, per precondition (2).
-    go_invis_tvbs _ (_:_) _ [] =
-      fail $ "dMatchUpSigWithDecl.go_invis_tvbs: Too few binders"
-    go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss@(decl_bndr:decl_bndrs) =
-      case dtvbFlag decl_bndr of
-        -- If the next decl_bndr is required, then we have a invisible forall in
-        -- the kind without a corresponding invisible @-binder, which is
-        -- allowed. In this case, we simply apply the substitution and recurse.
-        BndrReq -> do
+    go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss =
+      case decl_bndrss of
+        [] -> skip_invis_bndr
+        decl_bndr:decl_bndrs ->
+          case dtvbFlag decl_bndr of
+            BndrReq -> skip_invis_bndr
+            -- If the next decl_bndr is an invisible @-binder, then we must match it
+            -- against the invisible forall–bound variable in the kind.
+            BndrInvis -> do
+              let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr
+              sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs
+              pure (fmap Invisible sig_tvb : sig_args')
+      where
+        -- There is an invisible forall in the kind without a corresponding
+        -- invisible @-binder, which is allowed. In this case, we simply apply
+        -- the substitution and recurse.
+        skip_invis_bndr :: q [DTyVarBndr ForAllTyFlag]
+        skip_invis_bndr = do
           let (subst', invis_tvb') = SC.substTyVarBndr subst invis_tvb
           sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrss
           pure $ fmap Invisible invis_tvb' : sig_args'
-        -- If the next decl_bndr is an invisible @-binder, then we must match it
-        -- against the invisible forall–bound variable in the kind.
-        BndrInvis -> do
-          let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr
-          sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs
-          pure (fmap Invisible sig_tvb : sig_args')
 
     go_vis_tvbs :: DSubst -> [DTyVarBndrUnit] -> DFunArgs -> [DTyVarBndrVis] -> q [DTyVarBndr ForAllTyFlag]
     go_vis_tvbs subst [] sig_args decl_bndrs =
       go_fun_args subst sig_args decl_bndrs
     -- This should not happen, per precondition (1).
     go_vis_tvbs _ (_:_) _ [] =
-      fail $ "dMatchUpSigWithDecl.go_vis_tvbs: Too few binders"
+      fail "dMatchUpSigWithDecl.go_vis_tvbs: Too few binders"
     go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (decl_bndr:decl_bndrs) = do
       case dtvbFlag decl_bndr of
         -- If the next decl_bndr is required, then we must match it against the
@@ -2225,6 +2240,8 @@ dMatchUpSigWithDecl = go_fun_args M.empty
           pure ((Required <$ sig_tvb) : sig_args')
         -- We have a visible forall in the kind, but an invisible @-binder as
         -- the next decl_bndr. This is ill kinded, so throw an error.
+        --
+        -- This should not happen, per precondition (2).
         BndrInvis ->
           fail $ "dMatchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: "
               ++ show decl_bndr

Language/Haskell/TH/Desugar/Util.hs

@@ -44,8 +44,6 @@ import Language.Haskell.TH.Datatype.TyVarBndr
 import qualified Language.Haskell.TH.Desugar.OSet as OS
 import Language.Haskell.TH.Desugar.OSet (OSet)
 import Language.Haskell.TH.Instances ()
-import Language.Haskell.TH.Ppr ( PprFlag(..) )
-import qualified Language.Haskell.TH.PprLib as Ppr
 import Language.Haskell.TH.Syntax
 
 import qualified Control.Monad.Fail as Fail
@@ -63,6 +61,11 @@ import GHC.Classes ( IP )
 import GHC.Generics ( Generic )
 import Unsafe.Coerce ( unsafeCoerce )
 
+#if __GLASGOW_HASKELL__ >= 900
+import Language.Haskell.TH.Ppr ( PprFlag(..) )
+import qualified Language.Haskell.TH.PprLib as Ppr
+#endif
+
 #if __GLASGOW_HASKELL__ >= 906
 import GHC.Tuple ( Solo(MkSolo) )
 #elif __GLASGOW_HASKELL__ >= 900
@@ -693,7 +696,7 @@ matchUpSigWithDecl = go_fun_args Map.empty
       -> FunArgs -> [TyVarBndrVis] -> q [TyVarBndr_ ForAllTyFlag]
     go_fun_args _ FANil [] =
       pure []
-    -- This should not happen, per the function's precondition
+    -- This should not happen, per precondition (1).
     go_fun_args _ FANil decl_bndrs =
       fail $ "matchUpSigWithDecl.go_fun_args: Too many binders: " ++ show decl_bndrs
     -- GHC now disallows kind-level constraints, per this GHC proposal:
@@ -709,19 +712,31 @@ matchUpSigWithDecl = go_fun_args Map.empty
       go_invis_tvbs subst tvbs sig_args decl_bndrs
     go_fun_args subst (FAForalls (ForallVis tvbs) sig_args) decl_bndrs =
       go_vis_tvbs subst tvbs sig_args decl_bndrs
-    go_fun_args subst (FAAnon anon sig_args) (decl_bndr:decl_bndrs) = do
-      let decl_bndr_name = tvName decl_bndr
-          mb_decl_bndr_kind = extractTvbKind_maybe decl_bndr
-          anon' = applySubstitution subst anon
-
-          anon'' =
-            case mb_decl_bndr_kind of
-              Nothing -> anon'
-              Just decl_bndr_kind -> do
-                let mb_match_subst = matchTy decl_bndr_kind anon'
-                maybe decl_bndr_kind (`applySubstitution` decl_bndr_kind) mb_match_subst
-      sig_args' <- go_fun_args subst sig_args decl_bndrs
-      pure $ kindedTVFlag decl_bndr_name Required anon'' : sig_args'
+    go_fun_args subst (FAAnon anon sig_args) (decl_bndr:decl_bndrs) =
+      case tvFlag decl_bndr of
+        -- If the next decl_bndr is required, then we must match its kind (if
+        -- one is provided) against the anonymous kind argument.
+        BndrReq -> do
+          let decl_bndr_name = tvName decl_bndr
+              mb_decl_bndr_kind = extractTvbKind_maybe decl_bndr
+              anon' = applySubstitution subst anon
+
+              anon'' =
+                case mb_decl_bndr_kind of
+                  Nothing -> anon'
+                  Just decl_bndr_kind -> do
+                    let mb_match_subst = matchTy decl_bndr_kind anon'
+                    maybe decl_bndr_kind (`applySubstitution` decl_bndr_kind) mb_match_subst
+          sig_args' <- go_fun_args subst sig_args decl_bndrs
+          pure $ kindedTVFlag decl_bndr_name Required anon'' : sig_args'
+        -- We have a visible, anonymous argument in the kind, but an invisible
+        -- @-binder as the next decl_bndr. This is ill kinded, so throw an
+        -- error.
+        --
+        -- This should not happen, per precondition (2).
+        BndrInvis ->
+          fail $ "dMatchUpSigWithDecl.go_fun_args: Expected visible binder, encountered invisible binder: "
+              ++ show decl_bndr
     -- This should not happen, per precondition (1).
     go_fun_args _ _ [] =
       fail "matchUpSigWithDecl.go_fun_args: Too few binders"
@@ -734,24 +749,27 @@ matchUpSigWithDecl = go_fun_args Map.empty
       -> q [TyVarBndr_ ForAllTyFlag]
     go_invis_tvbs subst [] sig_args decl_bndrs =
       go_fun_args subst sig_args decl_bndrs
-    -- This should not happen, per precondition (2).
-    go_invis_tvbs _ (_:_) _ [] =
-      fail $ "matchUpSigWithDecl.go_invis_tvbs: Too few binders"
-    go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss@(decl_bndr:decl_bndrs) =
-      case tvFlag decl_bndr of
-        -- If the next decl_bndr is required, then we have a invisible forall in
-        -- the kind without a corresponding invisible @-binder, which is
-        -- allowed. In this case, we simply apply the substitution and recurse.
-        BndrReq -> do
+    go_invis_tvbs subst (invis_tvb:invis_tvbs) sig_args decl_bndrss =
+      case decl_bndrss of
+        [] -> skip_invis_bndr
+        decl_bndr:decl_bndrs ->
+          case tvFlag decl_bndr of
+            BndrReq -> skip_invis_bndr
+            -- If the next decl_bndr is an invisible @-binder, then we must match it
+            -- against the invisible forall–bound variable in the kind.
+            BndrInvis -> do
+              let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr
+              sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs
+              pure (mapTVFlag Invisible sig_tvb : sig_args')
+      where
+        -- There is an invisible forall in the kind without a corresponding
+        -- invisible @-binder, which is allowed. In this case, we simply apply
+        -- the substitution and recurse.
+        skip_invis_bndr :: q [TyVarBndr_ ForAllTyFlag]
+        skip_invis_bndr = do
           let (subst', invis_tvb') = substTvb subst invis_tvb
           sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrss
           pure $ mapTVFlag Invisible invis_tvb' : sig_args'
-        -- If the next decl_bndr is an invisible @-binder, then we must match it
-        -- against the invisible forall–bound variable in the kind.
-        BndrInvis -> do
-          let (subst', sig_tvb) = match_tvbs subst invis_tvb decl_bndr
-          sig_args' <- go_invis_tvbs subst' invis_tvbs sig_args decl_bndrs
-          pure (mapTVFlag Invisible sig_tvb : sig_args')
 
     go_vis_tvbs ::
          Map Name Type
@@ -763,7 +781,7 @@ matchUpSigWithDecl = go_fun_args Map.empty
       go_fun_args subst sig_args decl_bndrs
     -- This should not happen, per precondition (1).
     go_vis_tvbs _ (_:_) _ [] =
-      fail $ "matchUpSigWithDecl.go_vis_tvbs: Too few binders"
+      fail "matchUpSigWithDecl.go_vis_tvbs: Too few binders"
     go_vis_tvbs subst (vis_tvb:vis_tvbs) sig_args (decl_bndr:decl_bndrs) = do
       case tvFlag decl_bndr of
         -- If the next decl_bndr is required, then we must match it against the
@@ -774,6 +792,8 @@ matchUpSigWithDecl = go_fun_args Map.empty
           pure (mapTVFlag (const Required) sig_tvb : sig_args')
         -- We have a visible forall in the kind, but an invisible @-binder as
         -- the next decl_bndr. This is ill kinded, so throw an error.
+        --
+        -- This should not happen, per precondition (2).
         BndrInvis ->
           fail $ "matchUpSigWithDecl.go_vis_tvbs: Expected visible binder, encountered invisible binder: "
               ++ show decl_bndr
@@ -958,6 +978,7 @@ data ForAllTyFlag
 instance DefaultBndrFlag ForAllTyFlag where
   defaultBndrFlag = Required
 
+#if __GLASGOW_HASKELL__ >= 900
 instance PprFlag ForAllTyFlag where
   pprTyVarBndr (PlainTV nm vis) =
     pprForAllTyFlag vis (ppr nm)
@@ -968,6 +989,7 @@ pprForAllTyFlag :: ForAllTyFlag -> Ppr.Doc -> Ppr.Doc
 pprForAllTyFlag (Invisible SpecifiedSpec) d = Ppr.char '@' Ppr.<> d
 pprForAllTyFlag (Invisible InferredSpec)  d = Ppr.braces d
 pprForAllTyFlag Required                  d = d
+#endif
 
 -- | Convert a list of @'TyVarBndr' 'ForAllTyFlag'@s to a list of
 -- 'TyVarBndrSpec's, which is suitable for use in an invisible @forall@.

Test/Run.hs

@@ -811,6 +811,21 @@ test_t220 =
              [| False |])
 #endif
 
+-- A regression test for #228, which ensures that dMatchUpSAKWithDecl behaves
+-- as expected on code that looks like this:
+--
+-- @
+-- type D :: forall (a :: Type). Type
+-- data D
+-- @
+test_t228 :: Bool
+test_t228 =
+  let sak = DForallT (DForallInvis [DKindedTV (mkName "a") SpecifiedSpec (DConT ''Type)]) (DConT ''Type)
+      expected_bndrs = [DKindedTV (mkName "a") (Invisible SpecifiedSpec) (DConT ''Type)] in
+  case dMatchUpSAKWithDecl sak [] of
+    Nothing -> False
+    Just actual_bndrs -> expected_bndrs `eqTH` actual_bndrs
+
 -- Unit tests for functions that compute free variables (e.g., fvDType)
 test_fvs :: [Bool]
 test_fvs =
@@ -1062,6 +1077,8 @@ main = hspec $ do
     it "correctly reifies the type of a class method with an inferred type variable binder" $ test_t220
 #endif
 
+    it "correctly matches up an invisible forall without a corresponding @-binder" $ test_t228
+
     -- Remove map pprints here after switch to th-orphans
     zipWithM (\t t' -> it ("can do Type->DType->Type of " ++ t) $ t == t')
              $(sequence round_trip_types >>= Syn.lift . map pprint)