[Haskell-ELTE] Funkcionalis fuggosegek

[Dr. ERDI Gergo]

Hi,

Adott az alabbi ket tipusosztaly es peldanyaik:

class Lt x y b | x y -> b where
     _lt :: x -> y -> b
instance Lt Zero (Succ n) True
instance Lt n Zero False
instance (Lt x y b) => Lt (Succ x) (Succ y) b


class Divides q p b | q p -> b where
     _divides :: q -> p -> b
instance Divides (Succ q) Zero True
instance (Lt (Succ p) (Succ q) True) => Divides (Succ q) (Succ p) False
instance (Lt q (Succ p) True, Sub (Succ p) (Succ q) p', Divides (Succ q) p' b) => Divides (Succ q) (Succ p) b

es adott az alabbi modon definialt "2":

type N2 = Succ (Succ Zero)
n2 = undefined :: N2

Kerdesem, hogy mit jelent az alabbi hibauzenet, ha a _divides n2 n2 
tipusat akarom meghataroztatni a GHC-vel:

*Main> :t _divides n2 n2

Top level:
     Couldn't match expected type `True' against inferred type `False'
     When using functional dependencies to combine
       Lt n Zero False,
         arising from the dependency `x y -> b'
         in the instance declaration at TypeProg.hs:63:9
       Lt Zero Zero True,
         arising from a use of `_divides' at <interactive>:1:0-13

?

Kosz,
 	Cactus
-- 

   .--= ULLA! =-----------------.   `We are not here to give users what
    \     http://gergo.erdi.hu   \   they want'  -- RMS, at GUADEC 2001
     `---= gergo at erdi.hu =-------'
Mindennek magas a fénytörési mutatója, ami fénylik.