Bump `base` version to 4.9.0.0 (closes #11026)
[ghc.git] / testsuite / tests / typecheck / should_fail / T9260.hs
1 {-# LANGUAGE DataKinds, TypeOperators, GADTs #-}
2
3 module T9260 where
4
5 import GHC.TypeLits
6
7 data Fin n where
8 Fzero :: Fin (n + 1)
9 Fsucc :: Fin n -> Fin (n + 1)
10
11 test :: Fin 1
12 test = Fsucc Fzero
13
14 {- Only the second error is legitimate.
15
16 % ghc --version
17 The Glorious Glasgow Haskell Compilation System, version 7.8.2
18 % ghc -ignore-dot-ghci /tmp/Error.hs
19 [1 of 1] Compiling Error ( /tmp/Error.hs, /tmp/Error.o )
20
21 /tmp/Error.hs:12:8:
22 Couldn't match type ‘0’ with ‘1’
23 Expected type: Fin 1
24 Actual type: Fin (0 + 1)
25 In the expression: Fsucc Fzero
26 In an equation for ‘test’: test = Fsucc Fzero
27
28 /tmp/Error.hs:12:14:
29 Couldn't match type ‘1’ with ‘0’
30 Expected type: Fin 0
31 Actual type: Fin (0 + 1)
32 In the first argument of ‘Fsucc’, namely ‘Fzero’
33 In the expression: Fsucc Fzero
34 -}