summaryrefslogtreecommitdiff
path: root/testsuite
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite')
-rw-r--r--testsuite/tests/dependent/should_compile/T14556.hs38
-rw-r--r--testsuite/tests/dependent/should_compile/T14720.hs44
-rw-r--r--testsuite/tests/dependent/should_compile/all.T8
-rw-r--r--testsuite/tests/dependent/should_fail/RAE_T32a.stderr25
-rw-r--r--testsuite/tests/dependent/should_fail/all.T2
-rw-r--r--testsuite/tests/typecheck/should_compile/SplitWD.hs55
-rw-r--r--testsuite/tests/typecheck/should_compile/T13643.hs22
-rw-r--r--testsuite/tests/typecheck/should_compile/T14441.hs15
-rw-r--r--testsuite/tests/typecheck/should_compile/T14749.hs27
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T8
-rw-r--r--testsuite/tests/typecheck/should_fail/T12373.stderr8
-rw-r--r--testsuite/tests/typecheck/should_run/Typeable1.stderr3
12 files changed, 230 insertions, 25 deletions
diff --git a/testsuite/tests/dependent/should_compile/T14556.hs b/testsuite/tests/dependent/should_compile/T14556.hs
new file mode 100644
index 0000000000..eebbdca888
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14556.hs
@@ -0,0 +1,38 @@
+{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
+
+module T14556 where
+
+import Data.Kind
+import Data.Proxy
+
+data Fn a b where
+ IdSym :: Fn Type Type
+
+type family
+ (@@) (f::Fn k k') (a::k)::k' where
+ IdSym @@ a = a
+
+data KIND = X | FNARR KIND KIND
+
+data TY :: KIND -> Type where
+ ID :: TY (FNARR X X)
+ FNAPP :: TY (FNARR k k') -> TY k -> TY k'
+
+data TyRep (kind::KIND) :: TY kind -> Type where
+ TID :: TyRep (FNARR X X) ID
+ TFnApp :: TyRep (FNARR k k') f
+ -> TyRep k a
+ -> TyRep k' (FNAPP f a)
+
+type family
+ IK (kind::KIND) :: Type where
+ IK X = Type
+ IK (FNARR k k') = Fn (IK k) (IK k')
+
+type family
+ IT (ty::TY kind) :: IK kind where
+ IT ID = IdSym
+ IT (FNAPP f x) = IT f @@ IT x
+
+zero :: TyRep X a -> IT a
+zero = undefined
diff --git a/testsuite/tests/dependent/should_compile/T14720.hs b/testsuite/tests/dependent/should_compile/T14720.hs
new file mode 100644
index 0000000000..c26a184689
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14720.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14720 where
+
+import Data.Kind (Type)
+import Data.Type.Equality ((:~:)(..), sym, trans)
+import Data.Void
+
+data family Sing (z :: k)
+
+class Generic (a :: Type) where
+ type Rep a :: Type
+ from :: a -> Rep a
+ to :: Rep a -> a
+
+class PGeneric (a :: Type) where
+ type PFrom (x :: a) :: Rep a
+ type PTo (x :: Rep a) :: a
+
+class SGeneric k where
+ sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
+ sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
+
+class (PGeneric k, SGeneric k) => VGeneric k where
+ sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
+ sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
+
+data Decision a = Proved a
+ | Disproved (a -> Void)
+
+class SDecide k where
+ (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
+ default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
+ => Sing a -> Sing b -> Decision (a :~: b)
+ s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
+ Proved (Refl :: PFrom a :~: PFrom b) ->
+ case (sTof s1, sTof s2) of
+ (Refl, Refl) -> Proved Refl
+ Disproved contra -> Disproved (\Refl -> contra Refl)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 684602cc94..ab7ab3c8df 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -25,7 +25,9 @@ test('T11966', normal, compile, [''])
test('T12442', normal, compile, [''])
test('T13538', normal, compile, [''])
test('T12176', normal, compile, [''])
-test('T14038', expect_broken(14038), compile, [''])
+test('T14038', normal, compile, [''])
test('T12742', normal, compile, [''])
-test('T13910', expect_broken(13910), compile, [''])
-test('T13938', expect_broken(13938), compile, [''])
+test('T13910', normal, compile, [''])
+test('T13938', normal, compile, [''])
+test('T14556', normal, compile, [''])
+test('T14720', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
index cb94dd2854..046a1e1aa4 100644
--- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
+++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr
@@ -1,19 +1,18 @@
RAE_T32a.hs:28:1: error:
- Too many parameters to Sing:
- x is unexpected;
- expected only two parameters
- In the data instance declaration for ‘Sing’
+ • Expected kind ‘k0 -> *’,
+ but ‘Sing Sigma (Sigma p r)’ has kind ‘*’
+ • In the data instance declaration for ‘Sing’
RAE_T32a.hs:28:20: error:
- Expecting two more arguments to ‘Sigma’
- Expected a type, but
- ‘Sigma’ has kind
- ‘forall p -> TyPi p (MkStar p) -> *’
- In the first argument of ‘Sing’, namely ‘Sigma’
- In the data instance declaration for ‘Sing’
+ • Expecting two more arguments to ‘Sigma’
+ Expected a type, but
+ ‘Sigma’ has kind
+ ‘forall p -> TyPi p (MkStar p) -> *’
+ • In the first argument of ‘Sing’, namely ‘Sigma’
+ In the data instance declaration for ‘Sing’
RAE_T32a.hs:28:27: error:
- Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
- In the second argument of ‘Sing’, namely ‘(Sigma p r)’
- In the data instance declaration for ‘Sing’
+ • Expected kind ‘Sigma’, but ‘Sigma p r’ has kind ‘*’
+ • In the second argument of ‘Sing’, namely ‘(Sigma p r)’
+ In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 4eb426419d..e28b2df5cd 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,5 +1,5 @@
test('DepFail1', normal, compile_fail, [''])
-test('RAE_T32a', expect_broken(12919), compile_fail, [''])
+test('RAE_T32a', normal, compile_fail, [''])
test('TypeSkolEscape', normal, compile_fail, [''])
test('BadTelescope', normal, compile_fail, [''])
test('BadTelescope2', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/SplitWD.hs b/testsuite/tests/typecheck/should_compile/SplitWD.hs
new file mode 100644
index 0000000000..370b077b6e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/SplitWD.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators,
+ TypeFamilies, GADTs, StandaloneDeriving #-}
+
+module SplitWD where
+
+import Data.Kind ( Type )
+
+data Nat = Zero | Succ Nat
+
+type family a + b where
+ Zero + b = b
+ Succ a + b = Succ (a + b)
+infixl 6 +
+
+data Vec :: Type -> Nat -> Type where
+ VNil :: Vec a Zero
+ (:>) :: a -> Vec a n -> Vec a (Succ n)
+infixr 5 :>
+
+type family (xs :: Vec a n) +++ (ys :: Vec a m) :: Vec a (n + m) where
+ VNil +++ ys = ys
+ (x :> xs) +++ ys = x :> (xs +++ ys)
+infixr 5 +++
+
+data Exp :: Vec Type n -> Type -> Type where
+ Var :: Elem xs x -> Exp xs x
+
+data Elem :: forall a n. Vec a n -> a -> Type where
+ Here :: Elem (x :> xs) x
+ There :: Elem xs x -> Elem (y :> xs) x
+
+-- | @Length xs@ is a runtime witness for how long a vector @xs@ is.
+-- @LZ :: Length xs@ says that @xs@ is empty.
+-- @LS len :: Length xs@ tells you that @xs@ has one more element
+-- than @len@ says.
+-- A term of type @Length xs@ also serves as a proxy for @xs@.
+data Length :: forall a n. Vec a n -> Type where
+ LZ :: Length VNil
+ LS :: Length xs -> Length (x :> xs)
+
+deriving instance Show (Length xs)
+
+-- | Convert an expression typed in one context to one typed in a larger
+-- context. Operationally, this amounts to de Bruijn index shifting.
+-- As a proposition, this is the weakening lemma.
+shift :: forall ts2 t ty. Exp ts2 ty -> Exp (t :> ts2) ty
+shift = go LZ
+ where
+ go :: forall ts1 ty. Length ts1 -> Exp (ts1 +++ ts2) ty -> Exp (ts1 +++ t :> ts2) ty
+ go l_ts1 (Var v) = Var (shift_elem l_ts1 v)
+
+ shift_elem :: Length ts1 -> Elem (ts1 +++ ts2) x
+ -> Elem (ts1 +++ t :> ts2) x
+ shift_elem = undefined
+
diff --git a/testsuite/tests/typecheck/should_compile/T13643.hs b/testsuite/tests/typecheck/should_compile/T13643.hs
new file mode 100644
index 0000000000..d7cf1342c8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13643.hs
@@ -0,0 +1,22 @@
+{-# Language TypeFamilyDependencies #-}
+{-# Language RankNTypes #-}
+{-# Language KindSignatures #-}
+{-# Language DataKinds #-}
+{-# Language TypeInType #-}
+{-# Language GADTs #-}
+
+import Data.Kind (Type)
+
+data Code = I
+
+type family
+ Interp (a :: Code) = (res :: Type) | res -> a where
+ Interp I = Bool
+
+data T :: forall a. Interp a -> Type where
+ MkNat :: T False
+
+instance Show (T a) where show _ = "MkNat"
+
+main = do
+ print MkNat
diff --git a/testsuite/tests/typecheck/should_compile/T14441.hs b/testsuite/tests/typecheck/should_compile/T14441.hs
new file mode 100644
index 0000000000..047de1659f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14441.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14441 where
+
+import Data.Kind
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+data Prox (a :: k) = P
+
+type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
+$(return [])
+type instance DemoteX P = P
diff --git a/testsuite/tests/typecheck/should_compile/T14749.hs b/testsuite/tests/typecheck/should_compile/T14749.hs
new file mode 100644
index 0000000000..79bcce66ff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14749.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
+
+module T14749 where
+
+import Data.Kind
+
+data KIND = STAR | KIND :> KIND
+
+data Ty :: KIND -> Type where
+ TMaybe :: Ty (STAR :> STAR)
+ TApp :: Ty (a :> b) -> (Ty a -> Ty b)
+
+type family IK (k :: KIND) = (res :: Type) where
+ IK STAR = Type
+ IK (a:>b) = IK a -> IK b
+
+type family I (t :: Ty k) = (res :: IK k) where
+ I TMaybe = Maybe
+ I (TApp f a) = (I f) (I a)
+
+data TyRep (k :: KIND) (t :: Ty k) where
+ TyMaybe :: TyRep (STAR:>STAR) TMaybe
+ TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
+
+zero :: TyRep STAR a -> I a
+zero x = case x of
+ TyApp TyMaybe _ -> Nothing
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9a2ce73263..f4b7fe6aeb 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -536,7 +536,7 @@ test('T12797', normal, compile, [''])
test('T12850', normal, compile, [''])
test('T12911', normal, compile, [''])
test('T12925', normal, compile, [''])
-test('T12919', expect_broken(12919), compile, [''])
+test('T12919', normal, compile, [''])
test('T12936', normal, compile, [''])
test('T13050', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
test('T13083', normal, compile, [''])
@@ -568,7 +568,7 @@ test('T13651a', normal, compile, [''])
test('T13680', normal, compile, [''])
test('T13785', normal, compile, [''])
test('T13804', normal, compile, [''])
-test('T13822', expect_broken(14749), compile, [''])
+test('T13822', normal, compile, [''])
test('T13848', normal, compile, [''])
test('T13871', normal, compile, [''])
test('T13879', normal, compile, [''])
@@ -599,3 +599,7 @@ test('T14763', normal, compile, [''])
test('T14811', normal, compile, [''])
test('T14934', [extra_files(['T14934.hs', 'T14934a.hs'])], run_command,
['$MAKE -s --no-print-directory T14934'])
+test('T13643', normal, compile, [''])
+test('SplitWD', expect_broken(14119), compile, [''])
+test('T14441', normal, compile, [''])
+test('T14749', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12373.stderr b/testsuite/tests/typecheck/should_fail/T12373.stderr
index d3a4bb5e65..a2568d75f9 100644
--- a/testsuite/tests/typecheck/should_fail/T12373.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12373.stderr
@@ -2,10 +2,10 @@
T12373.hs:10:19: error:
• Couldn't match a lifted type with an unlifted type
When matching types
- a1 :: *
- MVar# RealWorld a0 :: TYPE 'UnliftedRep
- Expected type: (# State# RealWorld, a1 #)
- Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
+ a0 :: *
+ MVar# RealWorld a1 :: TYPE 'UnliftedRep
+ Expected type: (# State# RealWorld, a0 #)
+ Actual type: (# State# RealWorld, MVar# RealWorld a1 #)
• In the expression: newMVar# rw
In the first argument of ‘IO’, namely ‘(\ rw -> newMVar# rw)’
In the first argument of ‘(>>)’, namely ‘IO (\ rw -> newMVar# rw)’
diff --git a/testsuite/tests/typecheck/should_run/Typeable1.stderr b/testsuite/tests/typecheck/should_run/Typeable1.stderr
index 65f6fd4645..63f02dbeb6 100644
--- a/testsuite/tests/typecheck/should_run/Typeable1.stderr
+++ b/testsuite/tests/typecheck/should_run/Typeable1.stderr
@@ -1,7 +1,6 @@
Typeable1.hs:22:5: error:
- • Couldn't match kind ‘* -> (* -> *) -> (* -> *) -> * -> *’
- with ‘forall k. (* -> *) -> (k -> *) -> k -> *’
+ • Couldn't match type ‘ComposeK’ with ‘a3 b3’
Inaccessible code in
a pattern with pattern synonym:
App :: forall k2 (t :: k2).
View Lorry Controller Status