diff options
| author | Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io> | 2020-10-02 03:39:25 +0200 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-10-10 14:50:42 -0400 |
| commit | 22f218b729a751bc5e5965624a716fc542f502a5 (patch) | |
| tree | bc2fc6d95107c9dd6d47bea254b2aa7900462374 /testsuite/tests/linear | |
| parent | ea59fd4d0abe73e1127dcdd91855a39232e62d41 (diff) | |
| download | haskell-22f218b729a751bc5e5965624a716fc542f502a5.tar.gz | |
Linear types: fix quantification in GADTs (#18790)
Diffstat (limited to 'testsuite/tests/linear')
| -rw-r--r-- | testsuite/tests/linear/should_compile/MultConstructor.hs | 27 |
1 files changed, 21 insertions, 6 deletions
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 |