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