Commit 22f218b7 authored by Krzysztof Gogolewski's avatar Krzysztof Gogolewski Committed by Marge Bot

Linear types: fix quantification in GADTs (#18790)

parent ea59fd4d
......@@ -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.
......
......@@ -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
......
{-# 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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment