Linear types: fix quantification in GADTs (#18790)

3 files changed, 30 insertions, 9 deletions

diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 999d7b3287..9bd1fa64ac 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -31,6 +31,7 @@ module GHC.Rename.HsType (
         extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars,
         extractHsTysRdrTyVars, extractRdrKindSigVars, extractDataDefnKindVars,
         extractHsTvBndrs, extractHsTyArgRdrKiTyVars,
+        extractHsScaledTysRdrTyVars,
         forAllOrNothing, nubL
   ) where
 
@@ -1748,6 +1749,9 @@ extractHsTyArgRdrKiTyVars args
 extractHsTyRdrTyVars :: LHsType GhcPs -> FreeKiTyVars
 extractHsTyRdrTyVars ty = extract_lty ty []
 
+extractHsScaledTysRdrTyVars :: [HsScaled GhcPs (LHsType GhcPs)] -> FreeKiTyVars -> FreeKiTyVars
+extractHsScaledTysRdrTyVars args acc = foldr (\(HsScaled m ty) -> extract_lty ty . extract_hs_arrow m) acc args
+
 -- | Extracts the free type/kind variables from the kind signature of a HsType.
 --   This is used to implicitly quantify over @k@ in @type T = Nothing :: Maybe k@.
 -- The left-to-right order of variables is preserved.
@@ -1764,8 +1768,8 @@ extractHsTyRdrTyVarsKindVars (L _ ty) =
 -- | Extracts free type and kind variables from types in a list.
 -- When the same name occurs multiple times in the types, all occurrences
 -- are returned.
-extractHsTysRdrTyVars :: [LHsType GhcPs] -> FreeKiTyVars
-extractHsTysRdrTyVars tys = extract_ltys tys []
+extractHsTysRdrTyVars :: [LHsType GhcPs] -> FreeKiTyVars -> FreeKiTyVars
+extractHsTysRdrTyVars tys = extract_ltys tys
 
 -- Returns the free kind variables of any explicitly-kinded binders, returning
 -- variable occurrences in left-to-right order.
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 22b51ec30a..6605bf1993 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2213,7 +2213,9 @@ rnConDecl decl@(ConDeclGADT { con_names   = names
           -- See #14808.
         ; implicit_bndrs <- forAllOrNothing explicit_forall
             $ extractHsTvBndrs explicit_tkvs
-            $ extractHsTysRdrTyVars (theta ++ map hsScaledThing arg_tys ++ [res_ty])
+            $ extractHsTysRdrTyVars theta
+            $ extractHsScaledTysRdrTyVars arg_tys
+            $ extractHsTysRdrTyVars [res_ty] []
 
         ; let ctxt = ConDeclCtx new_names
 
diff --git a/testsuite/tests/linear/should_compile/MultConstructor.hs b/testsuite/tests/linear/should_compile/MultConstructor.hs
index 780c906099..66ac13697d 100644
--- a/testsuite/tests/linear/should_compile/MultConstructor.hs
+++ b/testsuite/tests/linear/should_compile/MultConstructor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTSyntax, DataKinds, LinearTypes, KindSignatures, ExplicitForAll #-}
+{-# LANGUAGE GADTs, DataKinds, LinearTypes, KindSignatures, ExplicitForAll, TypeApplications #-}
 module MultConstructor where
 
 import GHC.Types
@@ -6,8 +6,23 @@ import GHC.Types
 data T p a where
   MkT :: a %p -> T p a
 
-{-
-this currently fails
-g :: forall (b :: Type). T 'Many b %1 -> (b,b)
-g (MkT x) = (x,x)
--}
+data Existential a where  -- #18790
+  MkE :: a %p -> Existential a
+
+f1 :: forall (a :: Type). T 'Many a %1 -> (a,a)
+f1 (MkT x) = (x,x)
+
+f2 :: forall (a :: Type) m. T 'Many a %1 -> T m a
+f2 (MkT x) = MkT x
+
+f3 :: forall (a :: Type). a %1 -> T 'One a
+f3 = MkT
+
+g1 :: forall (a :: Type). a %1 -> Existential a
+g1 x = MkE x
+
+g2 :: forall (a :: Type). Existential a -> a
+g2 (MkE x) = x
+
+vta :: Int %1 -> Existential Int
+vta x = MkE @Int @'One x