FunDepsやらHaskellのTips

完全にメモ書き

conflictをなんとかしたい

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}

class Force a b | a -> b where
    force :: a -> b

data Zero
data Succ a

instance Force Zero Zero
instance (Force a a') => Force (Succ a) (Succ a')

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four

type family Add a b
type instance Add Zero b = b
type instance Add (Succ a) b = Succ (Add a b)

data NatEq a b
instance (Force a a',Force b b',Force (NatEqProxy a' b') z) => Force (NatEq a b) z

data NatEqProxy a b
instance Force (NatEqProxy a a) True
instance (Force False c) => Force (NatEqProxy a b) c

data True
data False
instance Force True True
instance Force False False

type Add1 = Add Four Five
type Add2 = Add Four Four
type Add3 = Add Five Four
add1 = (undefined :: Add1)
add2 = (undefined :: Add2)
comp1 = (undefined :: NatEq Add1 Add3)

Proxyだとかを一段挟む。

Conflictは、FunDepsのDeps式の部分(a b -> cとか)で、a bが包含関係に成らない場合、つまりアレなソレの時に言われるので、何とか逃げる。