Skip to content
Snippets Groups Projects
Commit 47796026 authored by Richard Eisenberg's avatar Richard Eisenberg
Browse files

Add test case for #8917

parent b0bcbc04
No related branches found
No related tags found
No related merge requests found
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators #-}
module T8917 where
data Nat = Zero | Succ Nat
type family a + b where
Zero + a = a
(Succ n) + m = Succ (n + m)
:load T8917
:seti -XDataKinds -XTypeOperators
:kind! Zero + Succ Zero
:kind! Succ (Zero + Zero)
\ No newline at end of file
Zero + Succ Zero :: Nat
= 'Succ 'Zero
Succ (Zero + Zero) :: Nat
= 'Succ 'Zero
......@@ -169,3 +169,4 @@ test('T8696', normal, ghci_script, ['T8696.script'])
test('T8776', normal, ghci_script, ['T8776.script'])
test('ghci059', normal, ghci_script, ['ghci059.script'])
test('T8831', expect_broken(8831), ghci_script, ['T8831.script'])
test('T8917', normal, ghci_script, ['T8917.script'])
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment