diff options
Diffstat (limited to 'testsuite/tests/linear')
100 files changed, 1387 insertions, 0 deletions
diff --git a/testsuite/tests/linear/Makefile b/testsuite/tests/linear/Makefile new file mode 100644 index 0000000000..9a36a1c5fe --- /dev/null +++ b/testsuite/tests/linear/Makefile @@ -0,0 +1,3 @@ +TOP=../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/linear/should_compile/Arity2.hs b/testsuite/tests/linear/should_compile/Arity2.hs new file mode 100644 index 0000000000..d764d5111a --- /dev/null +++ b/testsuite/tests/linear/should_compile/Arity2.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +module Arity2 where +{- +inplace/bin/ghc-stage1 -O2 -dcore-lint +-} + +--import GHC.Base + +data Id a = Id a + +(<$>) :: (a -> b) -> Id a -> Id b +(<$>) f (Id a) = Id (f a) + +(<*>) :: Id (a -> b) -> Id a -> Id b +(<*>) (Id a) (Id b) = Id (a b) + +data Q = Q () () +data S = S () + +-- Q only gets eta-expand once and then trapped +foo = Q <$> Id () <*> Id () + +-- This compiles fine +foo2 = S <$> Id () + +{- +[1 of 1] Compiling Arity2 ( linear-tests/Arity2.hs, linear-tests/Arity2.o ) + +linear-tests/Arity2.hs:21:7: error: + • Couldn't match type ‘() ⊸ Q’ with ‘() -> b’ + Expected type: Id (() -> b) + Actual type: Id (() ⊸ Q) + • In the first argument of ‘(<*>)’, namely ‘Q <$> Id ()’ + In the expression: Q <$> Id () <*> Id () + In an equation for ‘foo’: foo = Q <$> Id () <*> Id () + • Relevant bindings include + foo :: Id b (bound at linear-tests/Arity2.hs:21:1) + | +21 | foo = Q <$> Id () <*> Id () + | ^^^^^^^^^^^ +-} diff --git a/testsuite/tests/linear/should_compile/Branches.hs b/testsuite/tests/linear/should_compile/Branches.hs new file mode 100644 index 0000000000..ee08ade335 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Branches.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE LinearTypes #-} +module GuardTup where + +data Q = Q () + +mkQ :: () -> Q +mkQ = Q + +foo smart + | smart = mkQ + | otherwise = Q + +fooIf smart = if smart then mkQ else Q diff --git a/testsuite/tests/linear/should_compile/CSETest.hs b/testsuite/tests/linear/should_compile/CSETest.hs new file mode 100644 index 0000000000..3321dbd43d --- /dev/null +++ b/testsuite/tests/linear/should_compile/CSETest.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE UnicodeSyntax #-} +{- This test makes sure that if two expressions with conflicting types are + CSEd then appropiate things happen. -} +module CSETest where + +minimal :: a ⊸ a +minimal x = x + +maximal :: a -> a +maximal x = x diff --git a/testsuite/tests/linear/should_compile/Dollar2.hs b/testsuite/tests/linear/should_compile/Dollar2.hs new file mode 100644 index 0000000000..4cde3dcb45 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Dollar2.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +module Dollar2 where +{- +inplace/bin/ghc-stage1 -O2 -dcore-lint +-} + + +import GHC.Base + +data AB = A () | B () + +qux :: Bool +qux = True +{-# NOINLINE qux #-} + +foo = id $ ((if qux then A else B) $ ()) + +{- + +-} diff --git a/testsuite/tests/linear/should_compile/DollarDefault.hs b/testsuite/tests/linear/should_compile/DollarDefault.hs new file mode 100644 index 0000000000..dbe689566a --- /dev/null +++ b/testsuite/tests/linear/should_compile/DollarDefault.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE LinearTypes #-} +module DollarDefault where + +class C p where + cid :: p a a -> p a a + +instance C (->) where + cid = id + +foo = (cid $ id) $ () diff --git a/testsuite/tests/linear/should_compile/DollarTest.hs b/testsuite/tests/linear/should_compile/DollarTest.hs new file mode 100644 index 0000000000..bc15a4fead --- /dev/null +++ b/testsuite/tests/linear/should_compile/DollarTest.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE UnicodeSyntax #-} +module Dollar where +{- +Check $ interacting with multiplicity polymorphism. +This caused Core Lint error previously. +-} + +import GHC.Base + +data Q a = Q a + +data QU = QU () + +test = QU $ () + +qux = Q $ () diff --git a/testsuite/tests/linear/should_compile/Foldr.hs b/testsuite/tests/linear/should_compile/Foldr.hs new file mode 100644 index 0000000000..759256d5b2 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Foldr.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +module FoldrExample where +{- +inplace/bin/ghc-stage1 -O2 -dcore-lint +-} + +import GHC.Base +import Data.Maybe + +qux :: [Maybe Char] -> String +qux str = foldr (maybe id (:)) "" str + +{- + +[1 of 1] Compiling FoldrExample ( linear-tests/Foldr.hs, linear-tests/Foldr.o ) + +linear-tests/Foldr.hs:11:27: error: + • Couldn't match type ‘[Char] ⊸ [Char]’ with ‘[Char] -> [Char]’ + Expected type: Char -> [Char] -> [Char] + Actual type: Char ⊸ [Char] ⊸ [Char] + • In the second argument of ‘maybe’, namely ‘(:)’ + In the first argument of ‘foldr’, namely ‘(maybe id (:))’ + In the expression: foldr (maybe id (:)) "" str + | +11 | qux str = foldr (maybe id (:)) "" str + | ^^^ + +-} diff --git a/testsuite/tests/linear/should_compile/Iden.hs b/testsuite/tests/linear/should_compile/Iden.hs new file mode 100644 index 0000000000..3522a43c42 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Iden.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE LinearTypes #-} +module Foo where + +newtype HappyIdentity a = HappyIdentity a +happyIdentity = HappyIdentity diff --git a/testsuite/tests/linear/should_compile/Linear10.hs b/testsuite/tests/linear/should_compile/Linear10.hs new file mode 100644 index 0000000000..e76a344fb0 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear10.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE GADTs #-} +module Linear10 where + +data Unrestricted a where Unrestricted :: a -> Unrestricted a + +unrestrictedDup :: Unrestricted a ⊸ (a, a) +unrestrictedDup (Unrestricted a) = (a,a) diff --git a/testsuite/tests/linear/should_compile/Linear12.hs b/testsuite/tests/linear/should_compile/Linear12.hs new file mode 100644 index 0000000000..3f49e94948 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear12.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE GADTs #-} +module Linear12 where + +type N a = a ⊸ () + +consume :: a ⊸ N a ⊸ () +consume x k = k x + +data N' a where N :: N a ⊸ N' a + +consume' :: a ⊸ N' a ⊸ () +consume' x (N k) = k x + +data W = W (W ⊸ ()) + +wPlusTwo :: W ⊸ W +wPlusTwo n = W (\(W k) -> k n) + +data Nat = S Nat + +natPlusOne :: Nat ⊸ Nat +natPlusOne n = S n + +data D = D () + +mkD :: () ⊸ D +mkD x = D x + +data Odd = E Even +data Even = O Odd + +evenPlusOne :: Even ⊸ Odd +evenPlusOne e = E e diff --git a/testsuite/tests/linear/should_compile/Linear14.hs b/testsuite/tests/linear/should_compile/Linear14.hs new file mode 100644 index 0000000000..3a40212f75 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear14.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear14 where + +-- Inference-related behaviour. Slightly sub-optimal still. + +bind1 :: (d ⊸ (a ⊸ b) ⊸ c) ⊸ d ⊸ (a⊸b) ⊸ c +bind1 b x f = b x (\a -> f a) + +newtype I a = I a + +bind2 :: (d ⊸ (a ⊸ b) ⊸ c) ⊸ d ⊸ (I a⊸b) ⊸ c +bind2 b x f = b x (\a -> f (I a)) + +bind3 :: (d ⊸ I (a ⊸ b) ⊸ c) ⊸ d ⊸ (a⊸b) ⊸ c +bind3 b x f = b x (I (\a -> f a)) + +bind4 :: (d ⊸ I ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c +bind4 b x f = b x (I (\g -> f g)) + +bind5 :: (d ⊸ ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c +bind5 b x f = b x (\g -> f (\a -> g a)) + +bind6 :: (d ⊸ I ((a ⊸ a') ⊸ b) ⊸ c) ⊸ d ⊸ ((a⊸a')⊸b) ⊸ c +bind6 b x f = b x (I (\g -> f (\a -> g a))) diff --git a/testsuite/tests/linear/should_compile/Linear15.hs b/testsuite/tests/linear/should_compile/Linear15.hs new file mode 100644 index 0000000000..fb244fe8b3 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear15.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear15 where + +correctWhere :: Int ⊸ Int +correctWhere a = g a + where + f :: Int ⊸ Int + f x = x + + g :: Int ⊸ Int + g x = f x diff --git a/testsuite/tests/linear/should_compile/Linear16.hs b/testsuite/tests/linear/should_compile/Linear16.hs new file mode 100644 index 0000000000..8ed8b5b36c --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear16.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE RebindableSyntax #-} +module Linear16 where + +-- Rebindable do notation + +(>>=) :: a ⊸ (a ⊸ b) ⊸ b +(>>=) x f = f x + +-- `fail` is needed due to pattern matching on (); +-- ideally, it shouldn't be there. +fail :: a +fail = fail + +correctDo = do + x <- () + (y,z) <- ((),x) + () <- y + () <- z + () diff --git a/testsuite/tests/linear/should_compile/Linear1Rule.hs b/testsuite/tests/linear/should_compile/Linear1Rule.hs new file mode 100644 index 0000000000..0553c61e84 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear1Rule.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE LinearTypes #-} +module Linear1Rule where + +-- Test the 1 <= p rule +f :: a #-> b +f = f + +g :: a # p -> b +g x = f x diff --git a/testsuite/tests/linear/should_compile/Linear3.hs b/testsuite/tests/linear/should_compile/Linear3.hs new file mode 100644 index 0000000000..52b9571085 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear3.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear3 where + +correctApp1 :: (a⊸b) ⊸ a ⊸ b +correctApp1 f a = f a + +correctApp2 :: (a⊸a) -> a ⊸ a +correctApp2 f a = f (f a) + +correctApp3 :: Int ⊸ Int +correctApp3 x = f x + where + f :: Int ⊸ Int + f y = y + +correctApp4 :: Int ⊸ Int +correctApp4 x = f (f x) + where + f :: Int ⊸ Int + f y = y + +correctIf :: Bool ⊸ a ⊸ a +correctIf x n = + if x then n else n diff --git a/testsuite/tests/linear/should_compile/Linear4.hs b/testsuite/tests/linear/should_compile/Linear4.hs new file mode 100644 index 0000000000..7f025e0a0f --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear4.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE LambdaCase, GADTs #-} +module Linear4 where + +correctCase :: Bool ⊸ a ⊸ a +correctCase x n = + case x of + True -> n + False -> n diff --git a/testsuite/tests/linear/should_compile/Linear6.hs b/testsuite/tests/linear/should_compile/Linear6.hs new file mode 100644 index 0000000000..ea095237f5 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear6.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear6 where + +correctEqn :: Bool ⊸ Int ⊸ Int +correctEqn True n = n +correctEqn False n = n diff --git a/testsuite/tests/linear/should_compile/Linear8.hs b/testsuite/tests/linear/should_compile/Linear8.hs new file mode 100644 index 0000000000..a7b6bf95e0 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Linear8.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE LambdaCase #-} +module Linear8 where + +correctLCase :: Int ⊸ Bool -> Int +correctLCase n = \case + True -> n + False -> n diff --git a/testsuite/tests/linear/should_compile/LinearConstructors.hs b/testsuite/tests/linear/should_compile/LinearConstructors.hs new file mode 100644 index 0000000000..0e0f1b547e --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearConstructors.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE TupleSections #-} +module LinearConstructors where + +data T a b = MkT a b + +f1 :: a #-> b #-> T a b +f1 = MkT + +f2 :: a #-> b -> T a b +f2 = MkT + +f3 :: a -> b #-> T a b +f3 = MkT + +f4 :: a -> b -> T a b +f4 = MkT + +-- tuple sections +g1 :: a #-> b #-> (a, b, Int) +g1 = (,,0) + +g2 :: a #-> b -> (a, b, Int) +g2 = (,,0) + +g3 :: a -> b #-> (a, b, Int) +g3 = (,,0) + +g4 :: a -> b -> (a, b, Int) +g4 = (,,0) diff --git a/testsuite/tests/linear/should_compile/LinearEmptyCase.hs b/testsuite/tests/linear/should_compile/LinearEmptyCase.hs new file mode 100644 index 0000000000..daa1918b56 --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearEmptyCase.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE EmptyCase, LinearTypes #-} + +module LinearEmptyCase where + +data Void + +f :: a #-> Void -> b +f x y = case y of {} diff --git a/testsuite/tests/linear/should_compile/LinearGuards.hs b/testsuite/tests/linear/should_compile/LinearGuards.hs new file mode 100644 index 0000000000..fae1208176 --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearGuards.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE LinearTypes #-} +module LinearGuards where + +f :: Bool -> a #-> a +f b a | b = a + | True = a diff --git a/testsuite/tests/linear/should_compile/LinearLetRec.hs b/testsuite/tests/linear/should_compile/LinearLetRec.hs new file mode 100644 index 0000000000..e7cf71d324 --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearLetRec.hs @@ -0,0 +1,11 @@ +module NameCache where + +data Name = Name +data NameCache = NameCache !Int !Name + +extendOrigNameCache :: Name -> Name -> Name +extendOrigNameCache _ _ = Name + +initNameCache :: Int -> [Name] -> NameCache +initNameCache us names + = NameCache us (foldl extendOrigNameCache Name names) diff --git a/testsuite/tests/linear/should_compile/LinearPolyDollar.hs b/testsuite/tests/linear/should_compile/LinearPolyDollar.hs new file mode 100644 index 0000000000..7d14351cfc --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearPolyDollar.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE LinearTypes #-} + +module LinearPolyDollar where + +-- The goal of this test is to ensure that the special typing rule of ($) plays +-- well with multiplicity-polymorphic functions + +data F = F Bool + +x = F $ True diff --git a/testsuite/tests/linear/should_compile/LinearTH1.hs b/testsuite/tests/linear/should_compile/LinearTH1.hs new file mode 100644 index 0000000000..4f19b3b449 --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearTH1.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE LinearTypes, TemplateHaskell #-} +{-# LANGUAGE NoMonomorphismRestriction #-} + +module LinearTH1 where + +x1 = [t|Int -> Int|] diff --git a/testsuite/tests/linear/should_compile/LinearTH2.hs b/testsuite/tests/linear/should_compile/LinearTH2.hs new file mode 100644 index 0000000000..a35f9a1c7e --- /dev/null +++ b/testsuite/tests/linear/should_compile/LinearTH2.hs @@ -0,0 +1,4 @@ +{-# LANGUAGE LinearTypes, TemplateHaskell, RankNTypes #-} +module LinearTH2 where + +x1 = [t|forall p. Int # p -> Int|] diff --git a/testsuite/tests/linear/should_compile/List.hs b/testsuite/tests/linear/should_compile/List.hs new file mode 100644 index 0000000000..4d87dba896 --- /dev/null +++ b/testsuite/tests/linear/should_compile/List.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +module List where +{- +inplace/bin/ghc-stage1 -O2 -dcore-lint + +See Cabal:Distribution.Types.VersionRange:556 +-} + +import GHC.Base + +data J = J () + +j :: () -> J +j = J + +tup = (j, J) +tup2 = (J, j) + +tup3 = [j, J] +tup4 = [J, j] + +{- + +[1 of 1] Compiling List ( linear-tests/List.hs, linear-tests/List.o ) + +linear-tests/List.hs:17:12: error: + • Couldn't match expected type ‘() -> J’ with actual type ‘() ⊸ J’ + • In the expression: J + In the expression: [j, J] + In an equation for ‘tup3’: tup3 = [j, J] + | +17 | tup3 = [j, J] + | ^ + +linear-tests/List.hs:18:12: error: + • Couldn't match expected type ‘() ⊸ J’ with actual type ‘() -> J’ + • In the expression: j + In the expression: [J, j] + In an equation for ‘tup4’: tup4 = [J, j] + | +18 | tup4 = [J, j] + | ^ + +-} diff --git a/testsuite/tests/linear/should_compile/Makefile b/testsuite/tests/linear/should_compile/Makefile new file mode 100644 index 0000000000..9101fbd40a --- /dev/null +++ b/testsuite/tests/linear/should_compile/Makefile @@ -0,0 +1,3 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/linear/should_compile/MultConstructor.hs b/testsuite/tests/linear/should_compile/MultConstructor.hs new file mode 100644 index 0000000000..6e631774ba --- /dev/null +++ b/testsuite/tests/linear/should_compile/MultConstructor.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTSyntax, DataKinds, LinearTypes, KindSignatures, ExplicitForAll #-} +module MultConstructor where + +import GHC.Types + +data T p a where + MkT :: a # p -> T p a + +{- +this currently fails +g :: forall (b :: Type). T 'Many b #-> (b,b) +g (MkT x) = (x,x) +-} diff --git a/testsuite/tests/linear/should_compile/OldList.hs b/testsuite/tests/linear/should_compile/OldList.hs new file mode 100644 index 0000000000..2ed7b8aaf2 --- /dev/null +++ b/testsuite/tests/linear/should_compile/OldList.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude, ScopedTypeVariables, BangPatterns, RankNTypes #-} + +{- +This is a simplified version of Data.OldList module from base. +This caused an assertion failure in earlier version of linear +types implementation. +-} + +module Data.OldList where + +import GHC.Base + +sortBy :: forall a . (a -> a -> Ordering) -> [a] +sortBy cmp = [] + where + sequences (a:b:xs) + | a `cmp` b == GT = descending b [a] xs + | otherwise = ascending b (a:) xs + sequences xs = [xs] + +-- descending :: a -> [a] -> [a] -> [[a]] + descending a as (b:bs) + | a `cmp` b == GT = descending b (a:as) bs + descending a as bs = (a:as): sequences bs + + ascending :: a -> (forall i . [a] # i -> [a]) -> [a] -> [[a]] + ascending a as (b:bs) + | a `cmp` b /= GT = ascending b foo bs + where + foo :: [a] # k -> [a] + foo ys = as (a:ys) + ascending a as bs = let !x = as [a] + in x : sequences bs diff --git a/testsuite/tests/linear/should_compile/Op.hs b/testsuite/tests/linear/should_compile/Op.hs new file mode 100644 index 0000000000..725fd222d9 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Op.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +module Op where +{- +See Control.Arrow and Data.Functor.Contravariant +-} + +import GHC.Base + +class Or p where + or :: p a b -> p a b -> p a b + +instance Or (->) where + or x _ = x + + +foo = or Just (\x -> Just x) + +{- +This caused an error in the earlier version of linear types: + +linear-tests/Op.hs:18:16: error: + • Couldn't match expected type ‘a ⊸ Maybe a’ + with actual type ‘a0 -> Maybe a0’ + • The lambda expression ‘\ x -> Just x’ has one argument, + its type is ‘p0 a b0’, + it is specialized to ‘a ⊸ Maybe a’ + In the second argument of ‘or’, namely ‘(\ x -> Just x)’ + In the expression: or Just (\ x -> Just x) + • Relevant bindings include + foo :: a ⊸ Maybe a (bound at linear-tests/Op.hs:18:1) + | +18 | foo = or Just (\x -> Just x) + | ^^^^^^^^^^^^ +-} diff --git a/testsuite/tests/linear/should_compile/Pr110.hs b/testsuite/tests/linear/should_compile/Pr110.hs new file mode 100644 index 0000000000..a3311cb7b8 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Pr110.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE LinearTypes #-} +module Pr110 where + +data Bloop = Bloop Bool + +g :: Bloop #-> Bool +g (Bloop x) = x + +h :: Bool #-> Bloop +h x = Bloop x diff --git a/testsuite/tests/linear/should_compile/RankN.hs b/testsuite/tests/linear/should_compile/RankN.hs new file mode 100644 index 0000000000..cadefa5290 --- /dev/null +++ b/testsuite/tests/linear/should_compile/RankN.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE RankNTypes #-} +module RankN where +{- +inplace/bin/ghc-stage1 -O2 -dcore-lint +-} + +import GHC.Base +{- +class Data a where + gunfold :: (forall b r. c (b -> r) -> c r) + -> (forall r. r -> c r) + -> c a + +foo = 1 +{-# NOINLINE foo #-} + +instance Data [a] where + gunfold k z = k (k (z (:))) + + +--qux :: Identity (Int ⊸ Int) +qux = Identity Just + +app :: Identity (a -> b) -> Identity a -> Identity b +app (Identity f) (Identity a) = Identity (f a) + +example = app qux (Identity 5) + +--unqux :: Int ⊸ Int +unqux = Just + +unapp :: (a -> b) -> a -> b +unapp f a = f a + +example1 = unapp unqux 5 + +foo :: Identity (a -> b) -> a -> b +foo = runIdentity + +fooTest = foo (Identity Just) + +foo2 :: (a -> b) -> a -> b +foo2 = ($) + +fooTest2 = let f = Just in foo2 f +-} + +data Identity a = Identity { runIdentity :: a } + +extraTest = (id Identity) :: a -> Identity a diff --git a/testsuite/tests/linear/should_compile/T1735Min.hs b/testsuite/tests/linear/should_compile/T1735Min.hs new file mode 100644 index 0000000000..8800272328 --- /dev/null +++ b/testsuite/tests/linear/should_compile/T1735Min.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UndecidableInstances, Rank2Types, + KindSignatures, EmptyDataDecls, MultiParamTypeClasses, CPP #-} + +module T1735_Help.Basics where + +data Proxy a = Proxy + +class Data ctx a where + gunfold :: Proxy ctx + -> (forall b r. Data ctx b => c (b -> r) -> c r) + -> (forall r. r -> c r) + -> Constr + -> c a + + +newtype ID x = ID { unID :: x } + +fromConstrB :: Data ctx a + => Proxy ctx + -> (forall b. Data ctx b => b) + -> Constr + -> a +fromConstrB ctx f = unID . gunfold ctx k z + where + k c = ID (unID c f) + z = ID + +data Constr = Constr diff --git a/testsuite/tests/linear/should_compile/Tunboxer.hs b/testsuite/tests/linear/should_compile/Tunboxer.hs new file mode 100644 index 0000000000..c6bc7f5f38 --- /dev/null +++ b/testsuite/tests/linear/should_compile/Tunboxer.hs @@ -0,0 +1,11 @@ +{-# OPTIONS_GHC -O #-} +module TUnboxer where + +-- This checks that the multiplicity of unboxer inside MkId.wrapCo is correct. +-- The test is a minimized version of base/GHC/Event/PSQ.hs and requires -O. +newtype Unique = Unique Int + +data IntPSQ = Bin !Unique + +deleteView :: Unique -> () +deleteView k = Bin k `seq` () diff --git a/testsuite/tests/linear/should_compile/TupSection.hs b/testsuite/tests/linear/should_compile/TupSection.hs new file mode 100644 index 0000000000..ea401e6e97 --- /dev/null +++ b/testsuite/tests/linear/should_compile/TupSection.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE TupleSections #-} +module TupSection where +{- +inplace/bin/ghc-stage1 -O2 -dcore-lint +-} + +myAp :: (a -> b) -> a -> b +myAp f x = f x + +foo = myAp (,()) () + +qux = ("go2",) $ () diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T new file mode 100644 index 0000000000..8b11b9ccb9 --- /dev/null +++ b/testsuite/tests/linear/should_compile/all.T @@ -0,0 +1,37 @@ +broken_multiplicity_syntax = 94 # https://github.com/tweag/ghc/issues/94 + +test('anf', normal, compile, ['']) +test('Arity2', normal, compile, ['']) +test('Branches', normal, compile, ['']) +test('CSETest', normal, compile, ['']) +test('Dollar2', normal, compile, ['']) +test('DollarDefault', normal, compile, ['']) +test('DollarTest', normal, compile, ['']) +test('Foldr', normal, compile, ['']) +test('Iden', normal, compile, ['']) +test('List', normal, compile, ['']) +test('OldList', expect_broken(broken_multiplicity_syntax), compile, ['']) +test('Op', normal, compile, ['']) +test('RankN', normal, compile, ['']) +test('T1735Min', normal, compile, ['']) +test('TupSection', normal, compile, ['']) +test('Pr110', normal, compile, ['']) +test('Linear10', normal, compile, ['']) +test('Linear12', normal, compile, ['']) +test('Linear14', expect_broken(298), compile, ['']) +test('Linear15', normal, compile, ['']) +test('Linear16', normal, compile, ['']) +test('Linear3', normal, compile, ['']) +test('Linear4', expect_broken(20), compile, ['']) +test('Linear6', normal, compile, ['']) +test('Linear8', normal, compile, ['']) +test('LinearGuards', normal, compile, ['']) +test('LinearPolyDollar', normal, compile, ['']) +test('LinearConstructors', normal, compile, ['']) +test('Linear1Rule', expect_broken(broken_multiplicity_syntax), compile, ['']) +test('LinearEmptyCase', normal, compile, ['']) +test('Tunboxer', normal, compile, ['']) +test('MultConstructor', expect_broken(broken_multiplicity_syntax), compile, ['']) +test('LinearLetRec', expect_broken(405), compile, ['-O -dlinear-core-lint']) +test('LinearTH1', normal, compile, ['']) +test('LinearTH2', expect_broken(broken_multiplicity_syntax), compile, ['']) diff --git a/testsuite/tests/linear/should_compile/anf.hs b/testsuite/tests/linear/should_compile/anf.hs new file mode 100644 index 0000000000..9f1982e397 --- /dev/null +++ b/testsuite/tests/linear/should_compile/anf.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE LinearTypes #-} +-- !! Data constructors with strict fields +-- This test should use -funbox-strict-fields + +module Main ( main ) where + +main = print (g (f t)) + +t = MkT 1 2 (3,4) (MkS 5 6) + +g (MkT x _ _ _) = x + +data T = MkT Int !Int !(Int,Int) !(S Int) + +data S a = MkS a a + + +{-# NOINLINE f #-} +f :: T -> T -- Takes apart the thing and puts it + -- back together differently +f (MkT x y (a,b) (MkS p q)) = MkT a b (p,q) (MkS x y) diff --git a/testsuite/tests/linear/should_fail/Linear1.hs b/testsuite/tests/linear/should_fail/Linear1.hs new file mode 100644 index 0000000000..cdb7eed939 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear1.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE LambdaCase, GADTs #-} +{-# LANGUAGE RebindableSyntax #-} +module Linear1 where + + +-- Must fail: +incorrectDup :: a ⊸ (a,a) +incorrectDup x = (x,x) + +-- Must fail: +incorrectDrop :: a ⊸ () +incorrectDrop x = () diff --git a/testsuite/tests/linear/should_fail/Linear1.stderr b/testsuite/tests/linear/should_fail/Linear1.stderr new file mode 100644 index 0000000000..c549d75be3 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear1.stderr @@ -0,0 +1,10 @@ + +Linear1.hs:10:14: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectDup’: incorrectDup x = (x, x) + +Linear1.hs:14:15: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectDrop’: incorrectDrop x = () diff --git a/testsuite/tests/linear/should_fail/Linear11.hs b/testsuite/tests/linear/should_fail/Linear11.hs new file mode 100644 index 0000000000..67b930ac57 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear11.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear11 where + +data Unrestricted a where Unrestricted :: a -> Unrestricted a + +incorrectUnrestricted :: a ⊸ Unrestricted a +incorrectUnrestricted a = Unrestricted a + +data NotUnrestricted a where NotUnrestricted :: a ⊸ NotUnrestricted a + +incorrectUnrestrictedDup :: NotUnrestricted a ⊸ (a,a) +incorrectUnrestrictedDup (NotUnrestricted a) = (a,a) diff --git a/testsuite/tests/linear/should_fail/Linear11.stderr b/testsuite/tests/linear/should_fail/Linear11.stderr new file mode 100644 index 0000000000..cb52fa16f4 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear11.stderr @@ -0,0 +1,13 @@ + +Linear11.hs:9:23: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘a’ + • In an equation for ‘incorrectUnrestricted’: + incorrectUnrestricted a = Unrestricted a + +Linear11.hs:14:43: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘a’ + • In the pattern: NotUnrestricted a + In an equation for ‘incorrectUnrestrictedDup’: + incorrectUnrestrictedDup (NotUnrestricted a) = (a, a) diff --git a/testsuite/tests/linear/should_fail/Linear13.hs b/testsuite/tests/linear/should_fail/Linear13.hs new file mode 100644 index 0000000000..7b9e09c52b --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear13.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear13 where + +incorrectLet :: a ⊸ () +incorrectLet a = let x = a in () + +incorrectLetWithSignature :: (Bool->Bool) #-> () +incorrectLetWithSignature x = let y :: Bool->Bool; y = x in () + +incorrectLazyMatch :: (a,b) ⊸ b +incorrectLazyMatch x = let (a,b) = x in b + +incorrectCasePromotion :: (a,b) ⊸ b +incorrectCasePromotion x = case x of (a,b) -> b diff --git a/testsuite/tests/linear/should_fail/Linear13.stderr b/testsuite/tests/linear/should_fail/Linear13.stderr new file mode 100644 index 0000000000..a781c20da6 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear13.stderr @@ -0,0 +1,28 @@ + +Linear13.hs:6:14: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘a’ + • In an equation for ‘incorrectLet’: + incorrectLet a = let x = a in () + +Linear13.hs:9:27: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectLetWithSignature’: + incorrectLetWithSignature x + = let + y :: Bool -> Bool + y = x + in () + +Linear13.hs:12:20: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectLazyMatch’: + incorrectLazyMatch x = let (a, b) = x in b + +Linear13.hs:15:24: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectCasePromotion’: + incorrectCasePromotion x = case x of { (a, b) -> b } diff --git a/testsuite/tests/linear/should_fail/Linear17.hs b/testsuite/tests/linear/should_fail/Linear17.hs new file mode 100644 index 0000000000..1d8abfdb09 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear17.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE RebindableSyntax #-} +module Linear17 where + +-- Rebindable do notation + +(>>=) :: a ⊸ (a ⊸ b) ⊸ b +(>>=) x f = f x + +-- `fail` is needed due to pattern matching on (); +-- ideally, it shouldn't be there. +fail :: a +fail = fail + +incorrectDo1 = do + x <- () + (y,z) <- ((),()) + () <- y + () <- z + () + +incorrectDo2 = do + x <- () + (y,z) <- ((),x) + () <- y + () + +incorrectDo3 = do + x <- () + (y,z) <- (x,x) + () <- y + () <- z + () diff --git a/testsuite/tests/linear/should_fail/Linear17.stderr b/testsuite/tests/linear/should_fail/Linear17.stderr new file mode 100644 index 0000000000..12193e115b --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear17.stderr @@ -0,0 +1,45 @@ + +Linear17.hs:17:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In a stmt of a 'do' block: x <- () + In the expression: + do x <- () + (y, z) <- ((), ()) + () <- y + () <- z + .... + In an equation for ‘incorrectDo1’: + incorrectDo1 + = do x <- () + (y, z) <- ((), ()) + () <- y + .... + +Linear17.hs:25:6: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘z’ + • In the pattern: (y, z) + In a stmt of a 'do' block: (y, z) <- ((), x) + In the expression: + do x <- () + (y, z) <- ((), x) + () <- y + () + +Linear17.hs:30:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In a stmt of a 'do' block: x <- () + In the expression: + do x <- () + (y, z) <- (x, x) + () <- y + () <- z + .... + In an equation for ‘incorrectDo3’: + incorrectDo3 + = do x <- () + (y, z) <- (x, x) + () <- y + .... diff --git a/testsuite/tests/linear/should_fail/Linear2.hs b/testsuite/tests/linear/should_fail/Linear2.hs new file mode 100644 index 0000000000..bb6f525f01 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear2.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear2 where + +dup :: a -> (a,a) +dup x = (x,x) + +incorrectApp1 :: a ⊸ ((a,Int),(a,Int)) +incorrectApp1 x = dup (x,0) + +incorrectApp2 :: (a->b) -> a ⊸ b +incorrectApp2 f x = f x + +incorrectIf :: Bool -> Int ⊸ Int +incorrectIf x n = + if x then n else 0 diff --git a/testsuite/tests/linear/should_fail/Linear2.stderr b/testsuite/tests/linear/should_fail/Linear2.stderr new file mode 100644 index 0000000000..eec52922a0 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear2.stderr @@ -0,0 +1,16 @@ + +Linear2.hs:9:15: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectApp1’: incorrectApp1 x = dup (x, 0) + +Linear2.hs:12:17: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘incorrectApp2’: incorrectApp2 f x = f x + +Linear2.hs:15:15: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘n’ + • In an equation for ‘incorrectIf’: + incorrectIf x n = if x then n else 0 diff --git a/testsuite/tests/linear/should_fail/Linear5.hs b/testsuite/tests/linear/should_fail/Linear5.hs new file mode 100644 index 0000000000..ad0c80356c --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear5.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear5 where + +incorrectEqn :: Bool -> Int ⊸ Int +incorrectEqn True n = n +incorrectEqn False n = 0 diff --git a/testsuite/tests/linear/should_fail/Linear5.stderr b/testsuite/tests/linear/should_fail/Linear5.stderr new file mode 100644 index 0000000000..4de49fb9d9 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear5.stderr @@ -0,0 +1,5 @@ + +Linear5.hs:7:20: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘n’ + • In an equation for ‘incorrectEqn’: incorrectEqn False n = 0 diff --git a/testsuite/tests/linear/should_fail/Linear7.hs b/testsuite/tests/linear/should_fail/Linear7.hs new file mode 100644 index 0000000000..9ee6438b11 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear7.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE LambdaCase #-} +module Linear7 where + +incorrectLCase :: Int ⊸ Bool -> Int +incorrectLCase n = \case + True -> n + False -> 0 diff --git a/testsuite/tests/linear/should_fail/Linear7.stderr b/testsuite/tests/linear/should_fail/Linear7.stderr new file mode 100644 index 0000000000..9dc596477d --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear7.stderr @@ -0,0 +1,9 @@ + +Linear7.hs:7:16: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘n’ + • In an equation for ‘incorrectLCase’: + incorrectLCase n + = \case + True -> n + False -> 0 diff --git a/testsuite/tests/linear/should_fail/Linear9.hs b/testsuite/tests/linear/should_fail/Linear9.hs new file mode 100644 index 0000000000..011c58e837 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear9.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE UnicodeSyntax #-} +module Linear9 where + +fst :: (a,b) -> a +fst (a,_) = a + +incorrectFst :: (a,b) ⊸ a +incorrectFst (a,_) = a + +incorrectFstVar :: (a,b) ⊸ a +incorrectFstVar (a,b) = a + +incorrectFirstDup :: (a,b) ⊸ ((a,a),b) +incorrectFirstDup (a,b) = ((a,a),b) + +incorrectFstFst :: ((a,b),c) ⊸ a +incorrectFstFst ((a,_),_) = a + +data Test a + = Foo a a + | Bar a + +incorrectTestFst :: Test a ⊸ a +incorrectTestFst (Foo a _) = a +incorrectTestFst (Bar a) = a diff --git a/testsuite/tests/linear/should_fail/Linear9.stderr b/testsuite/tests/linear/should_fail/Linear9.stderr new file mode 100644 index 0000000000..ab13270ee3 --- /dev/null +++ b/testsuite/tests/linear/should_fail/Linear9.stderr @@ -0,0 +1,43 @@ + +Linear9.hs:9:17: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: _ + In the pattern: (a, _) + In an equation for ‘incorrectFst’: incorrectFst (a, _) = a + +Linear9.hs:12:20: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘b’ + • In the pattern: (a, b) + In an equation for ‘incorrectFstVar’: incorrectFstVar (a, b) = a + +Linear9.hs:15:20: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘a’ + • In the pattern: (a, b) + In an equation for ‘incorrectFirstDup’: + incorrectFirstDup (a, b) = ((a, a), b) + +Linear9.hs:18:21: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: _ + In the pattern: (a, _) + In the pattern: ((a, _), _) + +Linear9.hs:18:24: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: _ + In the pattern: ((a, _), _) + In an equation for ‘incorrectFstFst’: + incorrectFstFst ((a, _), _) = a + +Linear9.hs:25:25: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: _ + In the pattern: Foo a _ + In an equation for ‘incorrectTestFst’: + incorrectTestFst (Foo a _) = a diff --git a/testsuite/tests/linear/should_fail/LinearAsPat.hs b/testsuite/tests/linear/should_fail/LinearAsPat.hs new file mode 100644 index 0000000000..e756f4369f --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearAsPat.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE LinearTypes #-} + +module LinearAsPat where + +shouldFail :: Bool #-> Bool +shouldFail x@True = x diff --git a/testsuite/tests/linear/should_fail/LinearAsPat.stderr b/testsuite/tests/linear/should_fail/LinearAsPat.stderr new file mode 100644 index 0000000000..7d6cc245cf --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearAsPat.stderr @@ -0,0 +1,5 @@ + +LinearAsPat.hs:6:12: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In an equation for ‘shouldFail’: shouldFail x@True = x diff --git a/testsuite/tests/linear/should_fail/LinearBottomMult.hs b/testsuite/tests/linear/should_fail/LinearBottomMult.hs new file mode 100644 index 0000000000..03bf8731a7 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearBottomMult.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs, LinearTypes, ScopedTypeVariables, EmptyCase #-} +module LinearBottomMult where + +-- Check that _|_ * Many is not a subusage of One +-- +data Void +data U a where U :: a -> U a + +elim :: U a #-> () +elim (U _) = () + +f :: a #-> () +f x = elim (U (\(a :: Void) -> case a of {})) diff --git a/testsuite/tests/linear/should_fail/LinearBottomMult.stderr b/testsuite/tests/linear/should_fail/LinearBottomMult.stderr new file mode 100644 index 0000000000..fd846070d8 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearBottomMult.stderr @@ -0,0 +1,6 @@ + +LinearBottomMult.hs:13:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘f’: + f x = elim (U (\ (a :: Void) -> case a of)) diff --git a/testsuite/tests/linear/should_fail/LinearConfusedDollar.hs b/testsuite/tests/linear/should_fail/LinearConfusedDollar.hs new file mode 100644 index 0000000000..2cd1628eeb --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearConfusedDollar.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE LinearTypes #-} +module LinearConfusedDollar where + +-- When ($) becomes polymorphic in the multiplicity, then, this test case won't +-- hold anymore. But, as it stands, it produces untyped desugared code, hence +-- must be rejected. + +f :: a #-> a +f x = x + +g :: a #-> a +g x = f $ x diff --git a/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr b/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr new file mode 100644 index 0000000000..4abdd1c18c --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr @@ -0,0 +1,6 @@ + +LinearConfusedDollar.hs:12:7: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from an application + • In the expression: f $ x + In an equation for ‘g’: g x = f $ x diff --git a/testsuite/tests/linear/should_fail/LinearErrOrigin.hs b/testsuite/tests/linear/should_fail/LinearErrOrigin.hs new file mode 100644 index 0000000000..1eeb149959 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearErrOrigin.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE LinearTypes #-} +module LinearErrOrigin where + +-- The error message should mention "arising from multiplicity of x". + +foo :: (a # p -> b) -> a # q -> b +foo f x = f x diff --git a/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr b/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr new file mode 100644 index 0000000000..10b889a9a8 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearErrOrigin.stderr @@ -0,0 +1,16 @@ + +LinearErrOrigin.hs:7:7: error: + • Couldn't match type ‘p’ with ‘q’ arising from multiplicity of ‘x’ + ‘p’ is a rigid type variable bound by + the type signature for: + foo :: forall a b. (a -> b) -> a -> b + at LinearErrOrigin.hs:6:1-35 + ‘q’ is a rigid type variable bound by + the type signature for: + foo :: forall a b. (a -> b) -> a -> b + at LinearErrOrigin.hs:6:1-35 + • In an equation for ‘foo’: foo f x = f x + • Relevant bindings include + f :: a # p -> b (bound at LinearErrOrigin.hs:7:5) + foo :: (a # p -> b) -> a # q -> b + (bound at LinearErrOrigin.hs:7:1) diff --git a/testsuite/tests/linear/should_fail/LinearGADTNewtype.hs b/testsuite/tests/linear/should_fail/LinearGADTNewtype.hs new file mode 100644 index 0000000000..789b8cc3b6 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearGADTNewtype.hs @@ -0,0 +1,3 @@ +{-# LANGUAGE LinearTypes, GADTs #-} +newtype A where + A :: Int -> A diff --git a/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr b/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr new file mode 100644 index 0000000000..42207d4f72 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearGADTNewtype.stderr @@ -0,0 +1,5 @@ + +LinearGADTNewtype.hs:3:4: error: + • A newtype constructor must be linear + • In the definition of data constructor ‘A’ + In the newtype declaration for ‘A’ diff --git a/testsuite/tests/linear/should_fail/LinearIf.hs b/testsuite/tests/linear/should_fail/LinearIf.hs new file mode 100644 index 0000000000..b19873120c --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearIf.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE RebindableSyntax #-} + +module LinearIf where + +import Prelude (Bool(..), Char) + +ifThenElse :: Bool -> a -> a -> a +ifThenElse True x _ = x +ifThenElse False _ y = y + +f :: Bool #-> Char #-> Char #-> Char +f b x y = if b then x else y + -- 'f' ought to be unrestricted in all three arguments because it desugars to + -- > ifThenElse b x y diff --git a/testsuite/tests/linear/should_fail/LinearIf.stderr b/testsuite/tests/linear/should_fail/LinearIf.stderr new file mode 100644 index 0000000000..c34bec5f4d --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearIf.stderr @@ -0,0 +1,15 @@ + +LinearIf.hs:13:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘b’ + • In an equation for ‘f’: f b x y = if b then x else y + +LinearIf.hs:13:5: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘f’: f b x y = if b then x else y + +LinearIf.hs:13:7: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘y’ + • In an equation for ‘f’: f b x y = if b then x else y diff --git a/testsuite/tests/linear/should_fail/LinearKind.hs b/testsuite/tests/linear/should_fail/LinearKind.hs new file mode 100644 index 0000000000..a60554a7a7 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearKind.hs @@ -0,0 +1,4 @@ +{-# LANGUAGE LinearTypes, KindSignatures #-} +module LinearKind where + +data A :: * #-> * diff --git a/testsuite/tests/linear/should_fail/LinearKind.stderr b/testsuite/tests/linear/should_fail/LinearKind.stderr new file mode 100644 index 0000000000..5ac2825b21 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearKind.stderr @@ -0,0 +1,5 @@ + +LinearKind.hs:4:11: error: + • Linear arrows disallowed in kinds: * #-> * + • In the kind ‘* #-> *’ + In the data type declaration for ‘A’ diff --git a/testsuite/tests/linear/should_fail/LinearLazyPat.hs b/testsuite/tests/linear/should_fail/LinearLazyPat.hs new file mode 100644 index 0000000000..8ed4024c40 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearLazyPat.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE LinearTypes #-} +module LinearLazyPat where + +f :: (a,b) #-> (b,a) +f ~(x,y) = (y,x) diff --git a/testsuite/tests/linear/should_fail/LinearLazyPat.stderr b/testsuite/tests/linear/should_fail/LinearLazyPat.stderr new file mode 100644 index 0000000000..1893d10417 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearLazyPat.stderr @@ -0,0 +1,6 @@ + +LinearLazyPat.hs:5:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: ~(x, y) + In an equation for ‘f’: f ~(x, y) = (y, x) diff --git a/testsuite/tests/linear/should_fail/LinearLet.hs b/testsuite/tests/linear/should_fail/LinearLet.hs new file mode 100644 index 0000000000..bf822a8a6e --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearLet.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE LinearTypes #-} +module LinearLet where + +f :: a #-> (a,a) +f x = let y = x in (y,y) diff --git a/testsuite/tests/linear/should_fail/LinearLet.stderr b/testsuite/tests/linear/should_fail/LinearLet.stderr new file mode 100644 index 0000000000..3b94833d7e --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearLet.stderr @@ -0,0 +1,5 @@ + +LinearLet.hs:5:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘f’: f x = let y = x in (y, y) diff --git a/testsuite/tests/linear/should_fail/LinearNoExt.hs b/testsuite/tests/linear/should_fail/LinearNoExt.hs new file mode 100644 index 0000000000..2671246f21 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearNoExt.hs @@ -0,0 +1,3 @@ +module LinearNoExt where + +type T = a #-> a diff --git a/testsuite/tests/linear/should_fail/LinearNoExt.stderr b/testsuite/tests/linear/should_fail/LinearNoExt.stderr new file mode 100644 index 0000000000..452409586d --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearNoExt.stderr @@ -0,0 +1,3 @@ + +LinearNoExt.hs:3:12: error: + Enable LinearTypes to allow linear functions diff --git a/testsuite/tests/linear/should_fail/LinearPartialSig.hs b/testsuite/tests/linear/should_fail/LinearPartialSig.hs new file mode 100644 index 0000000000..01dbeddfba --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearPartialSig.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE LinearTypes #-} +module LinearPartialSig where + +-- We should suggest that _ :: Multiplicity +f :: a # _ -> a +f x = x diff --git a/testsuite/tests/linear/should_fail/LinearPartialSig.stderr b/testsuite/tests/linear/should_fail/LinearPartialSig.stderr new file mode 100644 index 0000000000..4d25260bf2 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearPartialSig.stderr @@ -0,0 +1,7 @@ + +LinearPartialSig.hs:5:13: error: + • Found type wildcard ‘_’ + standing for ‘'Many :: GHC.Types.Multiplicity’ + To use the inferred type, enable PartialTypeSignatures + • In the type ‘a # _ -> a’ + In the type signature: f :: a # _ -> a diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn.hs b/testsuite/tests/linear/should_fail/LinearPatSyn.hs new file mode 100644 index 0000000000..3e947dba2e --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearPatSyn.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE PatternSynonyms #-} + +module LinearPatSyn where + +-- Linearity and pattern synonyms should eventually play well together, but it +-- seems to require changes to the desugarer. So currently pattern synonyms are +-- disallowed in linear patterns. + +pattern P :: b #-> a #-> (a, b) +pattern P y x = (x, y) + +s :: (a, b) #-> (b, a) +s (P y x) = (y, x) diff --git a/testsuite/tests/linear/should_fail/LinearPatSyn.stderr b/testsuite/tests/linear/should_fail/LinearPatSyn.stderr new file mode 100644 index 0000000000..f7c3aab406 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearPatSyn.stderr @@ -0,0 +1,6 @@ + +LinearPatSyn.hs:14:4: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: P y x + In an equation for ‘s’: s (P y x) = (y, x) diff --git a/testsuite/tests/linear/should_fail/LinearPolyType.hs b/testsuite/tests/linear/should_fail/LinearPolyType.hs new file mode 100644 index 0000000000..bcf46eed9f --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearPolyType.hs @@ -0,0 +1,16 @@ +-- Source: https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-438125526 +{-# LANGUAGE LinearTypes, GADTs, KindSignatures, DataKinds, TypeFamilies, PolyKinds #-} +module LinearPolyType where + +import GHC.Types +data SBool :: Bool -> Type where + STrue :: SBool True + SFalse :: SBool False + +type family If b t f where + If True t _ = t + If False _ f = f + +dep :: SBool b -> Int # If b One Many -> Int +dep STrue x = x +dep SFalse _ = 0 diff --git a/testsuite/tests/linear/should_fail/LinearPolyType.stderr b/testsuite/tests/linear/should_fail/LinearPolyType.stderr new file mode 100644 index 0000000000..fab6dfcc9b --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearPolyType.stderr @@ -0,0 +1,3 @@ + +LinearPolyType.hs:15:1: error: + Multiplicity coercions are currently not supported diff --git a/testsuite/tests/linear/should_fail/LinearRecordUpdate.hs b/testsuite/tests/linear/should_fail/LinearRecordUpdate.hs new file mode 100644 index 0000000000..e143dbd604 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearRecordUpdate.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE LinearTypes #-} + +module LinearRecordUpdate where + +data R = R { x :: Int, y :: Bool } + +shouldFail :: R #-> R +shouldFail r = r { y = False } diff --git a/testsuite/tests/linear/should_fail/LinearRecordUpdate.stderr b/testsuite/tests/linear/should_fail/LinearRecordUpdate.stderr new file mode 100644 index 0000000000..aa32a9db68 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearRecordUpdate.stderr @@ -0,0 +1,5 @@ + +LinearRecordUpdate.hs:8:12: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘r’ + • In an equation for ‘shouldFail’: shouldFail r = r {y = False} diff --git a/testsuite/tests/linear/should_fail/LinearSeq.hs b/testsuite/tests/linear/should_fail/LinearSeq.hs new file mode 100644 index 0000000000..0f2ed39c93 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearSeq.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE LinearTypes #-} + +module LinearSeq where + +bad :: a #-> () +bad x = seq x () diff --git a/testsuite/tests/linear/should_fail/LinearSeq.stderr b/testsuite/tests/linear/should_fail/LinearSeq.stderr new file mode 100644 index 0000000000..f6b22b5999 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearSeq.stderr @@ -0,0 +1,5 @@ + +LinearSeq.hs:6:5: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘bad’: bad x = seq x () diff --git a/testsuite/tests/linear/should_fail/LinearSequenceExpr.hs b/testsuite/tests/linear/should_fail/LinearSequenceExpr.hs new file mode 100644 index 0000000000..ff3ac9cedb --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearSequenceExpr.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE OverloadedLists #-} + +module LinearSequenceExpr where + +f :: Char #-> Char #-> [Char] +f x y = [x .. y] +-- This ought to fail, because `fromList` in base, is unrestricted diff --git a/testsuite/tests/linear/should_fail/LinearSequenceExpr.stderr b/testsuite/tests/linear/should_fail/LinearSequenceExpr.stderr new file mode 100644 index 0000000000..a3fdb4d7df --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearSequenceExpr.stderr @@ -0,0 +1,10 @@ + +LinearSequenceExpr.hs:7:3: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘x’ + • In an equation for ‘f’: f x y = [x .. y] + +LinearSequenceExpr.hs:7:5: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from multiplicity of ‘y’ + • In an equation for ‘f’: f x y = [x .. y] diff --git a/testsuite/tests/linear/should_fail/LinearVar.hs b/testsuite/tests/linear/should_fail/LinearVar.hs new file mode 100644 index 0000000000..7b4cde3647 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearVar.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE LinearTypes #-} +module LinearVar where + +f :: a # m -> b +f = undefined :: a -> b diff --git a/testsuite/tests/linear/should_fail/LinearVar.stderr b/testsuite/tests/linear/should_fail/LinearVar.stderr new file mode 100644 index 0000000000..04014ce79b --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearVar.stderr @@ -0,0 +1,13 @@ + +LinearVar.hs:5:5: error: + • Couldn't match type ‘m’ with ‘'Many’ + ‘m’ is a rigid type variable bound by + the type signature for: + f :: forall a b. a -> b + at LinearVar.hs:4:1-16 + Expected type: a # m -> b + Actual type: a -> b + • In the expression: undefined :: a -> b + In an equation for ‘f’: f = undefined :: a -> b + • Relevant bindings include + f :: a # m -> b (bound at LinearVar.hs:5:1) diff --git a/testsuite/tests/linear/should_fail/LinearViewPattern.hs b/testsuite/tests/linear/should_fail/LinearViewPattern.hs new file mode 100644 index 0000000000..737393911b --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearViewPattern.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE LinearTypes #-} +{-# LANGUAGE ViewPatterns #-} + +module LinearViewPattern where + +-- This is probably inessential. We are just protecting against potential +-- incorrect Core being emitted by the desugarer. When we understand linear view +-- pattern better, we will probably want to remove this test. + +f :: Bool #-> Bool +f (not -> True) = True diff --git a/testsuite/tests/linear/should_fail/LinearViewPattern.stderr b/testsuite/tests/linear/should_fail/LinearViewPattern.stderr new file mode 100644 index 0000000000..c0aa969741 --- /dev/null +++ b/testsuite/tests/linear/should_fail/LinearViewPattern.stderr @@ -0,0 +1,6 @@ + +LinearViewPattern.hs:11:4: error: + • Couldn't match type ‘'Many’ with ‘'One’ + arising from a non-linear pattern + • In the pattern: not -> True + In an equation for ‘f’: f (not -> True) = True diff --git a/testsuite/tests/linear/should_fail/Makefile b/testsuite/tests/linear/should_fail/Makefile new file mode 100644 index 0000000000..9101fbd40a --- /dev/null +++ b/testsuite/tests/linear/should_fail/Makefile @@ -0,0 +1,3 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/linear/should_fail/TypeClass.hs b/testsuite/tests/linear/should_fail/TypeClass.hs new file mode 100644 index 0000000000..9752810dc4 --- /dev/null +++ b/testsuite/tests/linear/should_fail/TypeClass.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE UnicodeSyntax #-} +{-# LANGUAGE LinearTypes #-} +module Foo where + +data Either a b = Left a | Right b + +either :: (a -> c) -> (b -> c) -> Either a b -> c +either f g (Left a) = f a +either f g (Right b) = g b + +class Iden p where + iden :: p a a + +instance Iden (->) where + iden x = x + +class Cat p where + comp :: p b c -> p a b -> p a c + +instance Cat (->) where + comp f g = \x -> f (g x) + +class ArrowChoice a where + (+++) :: a b c -> a b' c' -> a (Either b b') (Either c c') + (|||) :: a b d -> a c d -> a (Either b c) d + +instance ArrowChoice (->) where +-- This doesn't work as |p| is inferred to be |-o| because of |Left|. +-- Then GHC complains that |f| is not the same type before it realises +-- that the overall type must be (->) +-- f +++ g = (Left `comp` f) ||| (Right `comp` g) + f +++ g = (comp @(->) Left f) ||| (comp @(->) Right g) + (|||) = either + + +-- This shouldn't work +foo :: a ⊸ a +foo = iden diff --git a/testsuite/tests/linear/should_fail/TypeClass.stderr b/testsuite/tests/linear/should_fail/TypeClass.stderr new file mode 100644 index 0000000000..97ff625686 --- /dev/null +++ b/testsuite/tests/linear/should_fail/TypeClass.stderr @@ -0,0 +1,5 @@ + +TypeClass.hs:45:7: error: + • No instance for (Iden (FUN 'One)) arising from a use of ‘iden’ + • In the expression: iden + In an equation for ‘foo’: foo = iden diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T new file mode 100644 index 0000000000..67906053dc --- /dev/null +++ b/testsuite/tests/linear/should_fail/all.T @@ -0,0 +1,29 @@ +broken_multiplicity_syntax = 94 # https://github.com/tweag/ghc/issues/94 + +test('TypeClass', normal, compile_fail, ['']) +test('Linear11', normal, compile_fail, ['']) +test('Linear13', normal, compile_fail, ['']) +test('Linear17', normal, compile_fail, ['']) +test('Linear1', normal, compile_fail, ['']) +test('Linear2', normal, compile_fail, ['']) +test('Linear5', normal, compile_fail, ['']) +test('Linear7', normal, compile_fail, ['']) +test('Linear9', normal, compile_fail, ['']) +test('LinearNoExt', normal, compile_fail, ['']) +test('LinearAsPat', normal, compile_fail, ['']) +test('LinearLet', normal, compile_fail, ['']) +test('LinearLazyPat', normal, compile_fail, ['']) +test('LinearRecordUpdate', normal, compile_fail, ['']) +test('LinearSeq', normal, compile_fail, ['']) +test('LinearViewPattern', normal, compile_fail, ['']) +test('LinearConfusedDollar', normal, compile_fail, ['']) +test('LinearPatSyn', normal, compile_fail, ['']) +test('LinearGADTNewtype', normal, compile_fail, ['']) +test('LinearPartialSig', expect_broken(broken_multiplicity_syntax), compile_fail, ['']) +test('LinearKind', normal, compile_fail, ['']) +test('LinearVar', expect_broken(broken_multiplicity_syntax), compile_fail, ['']) +test('LinearErrOrigin', expect_broken(broken_multiplicity_syntax), compile_fail, ['']) +test('LinearPolyType', expect_broken([436, broken_multiplicity_syntax]), compile_fail, ['']) # not supported yet (#354) +test('LinearBottomMult', normal, compile_fail, ['']) +test('LinearSequenceExpr', normal, compile_fail, ['']) +test('LinearIf', normal, compile_fail, ['']) diff --git a/testsuite/tests/linear/should_run/LinearGhci.script b/testsuite/tests/linear/should_run/LinearGhci.script new file mode 100644 index 0000000000..78f81ef8d2 --- /dev/null +++ b/testsuite/tests/linear/should_run/LinearGhci.script @@ -0,0 +1,11 @@ +data T a = MkT a +:type +v MkT +:set -XLinearTypes +:type +v MkT +:set -XGADTs +data T a where MkT :: a #-> a -> T a +:info T +data T a b m n r = MkT a b m n r +:set -fprint-explicit-foralls +-- check that user variables are not renamed (see dataConMulVars) +:type +v MkT diff --git a/testsuite/tests/linear/should_run/LinearGhci.stdout b/testsuite/tests/linear/should_run/LinearGhci.stdout new file mode 100644 index 0000000000..ed5c9cfe64 --- /dev/null +++ b/testsuite/tests/linear/should_run/LinearGhci.stdout @@ -0,0 +1,7 @@ +MkT :: a -> T a +MkT :: a -> T a +type T :: * -> * +data T a where + MkT :: a #-> a -> T a + -- Defined at <interactive>:6:1 +MkT :: forall a b m n r. a -> b -> m -> n -> r -> T a b m n r diff --git a/testsuite/tests/linear/should_run/LinearTypeable.hs b/testsuite/tests/linear/should_run/LinearTypeable.hs new file mode 100644 index 0000000000..69772f7b33 --- /dev/null +++ b/testsuite/tests/linear/should_run/LinearTypeable.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE LinearTypes, TypeOperators #-} +module Main (main) where + +import Data.Typeable +import Data.Maybe + +x :: Maybe ((Int -> Int) :~: (Int #-> Int)) +x = eqT + +main = print (isJust x) diff --git a/testsuite/tests/linear/should_run/LinearTypeable.stdout b/testsuite/tests/linear/should_run/LinearTypeable.stdout new file mode 100644 index 0000000000..bc59c12aa1 --- /dev/null +++ b/testsuite/tests/linear/should_run/LinearTypeable.stdout @@ -0,0 +1 @@ +False diff --git a/testsuite/tests/linear/should_run/Makefile b/testsuite/tests/linear/should_run/Makefile new file mode 100644 index 0000000000..9101fbd40a --- /dev/null +++ b/testsuite/tests/linear/should_run/Makefile @@ -0,0 +1,3 @@ +TOP=../../.. +include $(TOP)/mk/boilerplate.mk +include $(TOP)/mk/test.mk diff --git a/testsuite/tests/linear/should_run/all.T b/testsuite/tests/linear/should_run/all.T new file mode 100644 index 0000000000..1fbe20581c --- /dev/null +++ b/testsuite/tests/linear/should_run/all.T @@ -0,0 +1,2 @@ +test('LinearTypeable', normal, compile_and_run, ['']) +test('LinearGhci', normal, ghci_script, ['LinearGhci.script']) |