Commit 68f198f5 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Test case for #7961.

Test case: dependent/shoud_compile/TypeLevelVec
parent a459451f
{-# LANGUAGE TypeInType, UnicodeSyntax, GADTs, NoImplicitPrelude,
TypeOperators, TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module TypeLevelVec where
import Data.Kind
data Type where
O
S
type family x + y where
O + n = n
S m + n = S (m + n)
infixl 5 +
data Vec Type Type where
Nil Vec O a
(:>) a Vec n a Vec (S n) a
infixr 8 :>
type family (x Vec n a) ++ (y Vec m a) Vec (n + m) a where
Nil ++ y = y
(x :> xs) ++ y = x :> (xs ++ y)
infixl 5 ++
......@@ -8,3 +8,4 @@ test('RAE_T32b', only_ways('normal'), compile, [''])
test('KindLevels', normal, compile, [''])
test('RaeBlogPost', normal, compile, [''])
test('mkGADTVars', normal, compile, [''])
test('TypeLevelVec',normal,compile, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment