Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / TypeLevelVec.hs
1 {-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude,
2 TypeOperators, TypeFamilies #-}
3 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
4
5 module TypeLevelVec where
6
7 import Data.Kind
8
9 data ℕ ∷ Type where
10 O ∷ ℕ
11 S ∷ ℕ → ℕ
12
13 type family x + y where
14 O + n = n
15 S m + n = S (m + n)
16 infixl 5 +
17
18 data Vec ∷ ℕ → Type → Type where
19 Nil ∷ Vec O a
20 (:>) ∷ a → Vec n a → Vec (S n) a
21 infixr 8 :>
22
23 type family (x ∷ Vec n a) ++ (y ∷ Vec m a) ∷ Vec (n + m) a where
24 Nil ++ y = y
25 (x :> xs) ++ y = x :> (xs ++ y)
26 infixl 5 ++