diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-03-27 08:52:15 -0400 |
---|---|---|
committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-03-27 08:52:21 -0400 |
commit | 3ebf05f5410a3e89d4dc6d451aea5020706fa5b0 (patch) | |
tree | 8d1227b9f5f6508d3bd878ab20300423c100d5ae | |
parent | a7628dcd2cb570fe41de247af6aa71a89177a9b9 (diff) | |
download | haskell-3ebf05f5410a3e89d4dc6d451aea5020706fa5b0.tar.gz |
Fix the test for #13938
Only half of the test files were checked in for T13938.
This commit adds the missing half.
-rw-r--r-- | testsuite/tests/dependent/should_compile/Makefile | 5 | ||||
-rw-r--r-- | testsuite/tests/dependent/should_compile/T13938.hs | 82 | ||||
-rw-r--r-- | testsuite/tests/dependent/should_compile/T13938a.hs | 80 | ||||
-rw-r--r-- | testsuite/tests/dependent/should_compile/all.T | 3 |
4 files changed, 102 insertions, 68 deletions
diff --git a/testsuite/tests/dependent/should_compile/Makefile b/testsuite/tests/dependent/should_compile/Makefile index 9101fbd40a..0f855180c0 100644 --- a/testsuite/tests/dependent/should_compile/Makefile +++ b/testsuite/tests/dependent/should_compile/Makefile @@ -1,3 +1,8 @@ TOP=../../.. include $(TOP)/mk/boilerplate.mk include $(TOP)/mk/test.mk + +T13938: + $(RM) T13938a.hi T13938a.o T13938.hi T13938.o + '$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938a.hs + '$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938.hs diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs index 3ba9e273e4..dd4f3d6c7c 100644 --- a/testsuite/tests/dependent/should_compile/T13938.hs +++ b/testsuite/tests/dependent/should_compile/T13938.hs @@ -1,80 +1,28 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} module T13938 where -import Data.Kind (Type) +import T13938a +import Data.Kind +import Data.Type.Equality +import GHC.TypeLits -data family Sing (a :: k) -data instance Sing (z :: [a]) where - SNil :: Sing '[] - SCons :: Sing x -> Sing xs -> Sing (x:xs) +type family Length (l :: [a]) :: Nat where {} +type family Map (f :: a ~> b) (l :: [a]) :: [b] where {} -data TyFun :: Type -> Type -> Type -type a ~> b = TyFun a b -> Type -infixr 0 ~> +type WhyMapPreservesLength (f :: x ~> y) (l :: [x]) + = Length l :~: Length (Map f l) +data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type +type instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l -type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 -type a @@ b = Apply a b -infixl 9 @@ - -data FunArrow = (:->) -- ^ '(->)' - | (:~>) -- ^ '(~>)' - -class FunType (arr :: FunArrow) where - type Fun (k1 :: Type) arr (k2 :: Type) :: Type - -class FunType arr => AppType (arr :: FunArrow) where - type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 - -type FunApp arr = (FunType arr, AppType arr) - -instance FunType (:->) where - type Fun k1 (:->) k2 = k1 -> k2 - -$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter - -instance AppType (:->) where - type App k1 (:->) k2 (f :: k1 -> k2) x = f x - -instance FunType (:~>) where - type Fun k1 (:~>) k2 = k1 ~> k2 - -$(return []) - -instance AppType (:~>) where - type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x - -infixr 0 -?> -type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 - -elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). - Sing l - -> p '[] - -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs)) - -> p l -elimList = elimListPoly @(:->) - -elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). - Sing l - -> p @@ '[] - -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs)) - -> p @@ l -elimListTyFun = elimListPoly @(:~>) @_ @p - -elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). - FunApp arr - => Sing l - -> App [a] arr Type p '[] - -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs)) - -> App [a] arr Type p l -elimListPoly SNil pNil _ = pNil -elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons) +mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]). + Length l :~: Length (Map f l) +mapPreservesLength + = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs new file mode 100644 index 0000000000..3a09292922 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T13938a.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +module T13938a where + +import Data.Kind (Type) + +data family Sing (a :: k) +data instance Sing (z :: [a]) where + SNil :: Sing '[] + SCons :: Sing x -> Sing xs -> Sing (x:xs) + +data TyFun :: Type -> Type -> Type +type a ~> b = TyFun a b -> Type +infixr 0 ~> + +type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 +type a @@ b = Apply a b +infixl 9 @@ + +data FunArrow = (:->) -- ^ '(->)' + | (:~>) -- ^ '(~>)' + +class FunType (arr :: FunArrow) where + type Fun (k1 :: Type) arr (k2 :: Type) :: Type + +class FunType arr => AppType (arr :: FunArrow) where + type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2 + +type FunApp arr = (FunType arr, AppType arr) + +instance FunType (:->) where + type Fun k1 (:->) k2 = k1 -> k2 + +$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter + +instance AppType (:->) where + type App k1 (:->) k2 (f :: k1 -> k2) x = f x + +instance FunType (:~>) where + type Fun k1 (:~>) k2 = k1 ~> k2 + +$(return []) + +instance AppType (:~>) where + type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x + +infixr 0 -?> +type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2 + +elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]). + Sing l + -> p '[] + -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs)) + -> p l +elimList = elimListPoly @(:->) + +elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]). + Sing l + -> p @@ '[] + -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs)) + -> p @@ l +elimListTyFun = elimListPoly @(:~>) @_ @p + +elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]). + FunApp arr + => Sing l + -> App [a] arr Type p '[] + -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs)) + -> App [a] arr Type p l +elimListPoly SNil pNil _ = pNil +elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons) diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index ab7ab3c8df..da25b22799 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -28,6 +28,7 @@ test('T12176', normal, compile, ['']) test('T14038', normal, compile, ['']) test('T12742', normal, compile, ['']) test('T13910', normal, compile, ['']) -test('T13938', normal, compile, ['']) +test('T13938', [extra_files(['T13938a.hs'])], run_command, + ['$MAKE -s --no-print-directory T13938']) test('T14556', normal, compile, ['']) test('T14720', normal, compile, ['']) |