diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2015-12-18 15:30:45 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2015-12-18 15:39:33 +0000 |
commit | 9d921d6bfeec8320f7ad5e4532bf4edadc7f92cd (patch) | |
tree | 2b25192313a7b26934e8fe4cf1b61dfd1c7cbc66 | |
parent | f857d27affd545cf9a55de69c7147204c046cb8d (diff) | |
download | haskell-9d921d6bfeec8320f7ad5e4532bf4edadc7f92cd.tar.gz |
Test Trac #11248, #11249
-rw-r--r-- | testsuite/tests/polykinds/T11248.hs | 43 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T11249.hs | 40 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 3 |
3 files changed, 86 insertions, 0 deletions
diff --git a/testsuite/tests/polykinds/T11248.hs b/testsuite/tests/polykinds/T11248.hs new file mode 100644 index 0000000000..e1c8fcc1b8 --- /dev/null +++ b/testsuite/tests/polykinds/T11248.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, + KindSignatures, ConstraintKinds #-} + +module T11248 where + +import GHC.TypeLits + +type a / b = FDiv a b +type a ** b = FMul a b + +type family FDiv a b where + FDiv 11648 128 = 91 + +type family FMul a b where + FMul 64 91 = 5824 + +type family FGCD a b where + FGCD 128 448 = 64 + FGCD 128 5824 = 64 + +type family FLCM a b where + FLCM 128 5824 = 11648 + +data CT (m :: Nat) (m' :: Nat) +type H0 = 128 +type H1 = 448 +type H0' = 11648 +type H1' = 5824 + +main' = let x = undefined :: CT H0 H0' + in foo x :: CT H1 H1' + +foo x = bug x + +type Ctx2 e r s e' r' = + (e ~ FGCD r e', r' ~ FLCM r e', e ~ FGCD r s) + +type Ctx1 e r s e' r' = + (Ctx2 e r s e' r', e' ~ (e ** (r' / r))) + +bug :: (Ctx1 e r s e' r') + => CT r r' -> CT s s' +bug = undefined diff --git a/testsuite/tests/polykinds/T11249.hs b/testsuite/tests/polykinds/T11249.hs new file mode 100644 index 0000000000..7bc9d4fc7b --- /dev/null +++ b/testsuite/tests/polykinds/T11249.hs @@ -0,0 +1,40 @@ +{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, + KindSignatures, ConstraintKinds #-} + +module T11249 where + +import GHC.TypeLits + +type a / b = FDiv a b +type a ** b = FMul a b + +type family FDiv a b where + FDiv 11648 128 = 91 + +type family FMul a b where + FMul 64 91 = 5824 + +type family FGCD a b where + FGCD 128 448 = 64 + FGCD 128 5824 = 64 + +type family FLCM a b where + FLCM 128 5824 = 11648 + +data CT (m :: Nat) (m' :: Nat) +type H0 = 128 +type H1 = 448 +type H0' = 11648 +type H1' = 5824 + +main' = let x = undefined :: CT H0 H0' + in foo x :: CT H1 H1' + +foo x = bug x + +type Ctx2 e r s e' r' = + (e ~ FGCD r e', r' ~ FLCM r e', e ~ FGCD r s) + +bug :: (Ctx2 e r s e' r', e' ~ (e ** (FDiv r' r))) + => CT r r' -> CT s s' +bug = undefined diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index d0aa124b90..fd7b2162ff 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -127,3 +127,6 @@ test('T11142', normal, compile_fail, ['']) test('SigTvKinds', normal, compile, ['']) test('SigTvKinds2', expect_broken(11203), compile_fail, ['']) test('T9017', normal, compile_fail, ['']) +test('T11249', normal, compile, ['']) +test('T11248', normal, compile, ['']) + |