From 22f218b729a751bc5e5965624a716fc542f502a5 Mon Sep 17 00:00:00 2001 From: Krzysztof Gogolewski Date: Fri, 2 Oct 2020 03:39:25 +0200 Subject: Linear types: fix quantification in GADTs (#18790) --- .../tests/linear/should_compile/MultConstructor.hs | 27 +++++++++++++++++----- 1 file changed, 21 insertions(+), 6 deletions(-) (limited to 'testsuite/tests/linear') 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 -- cgit v1.2.1