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 -}