Вопрос по type families.

[Alexander V Vershilov]

Здравствуйте.

У меня возникла проблема по поводу попытки переписать код, использующий
OverlappingInstances используя closed type families, так чтобы
избавиться от OverlappingInstances.

Но решить задачу в полной мере мне не удалось, упрощенная выжимка выглядит
так:

> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE TypeFamilies #-}

> data K s m v = K (m v) deriving (Monad,Applicative,Functor)

> runK :: (forall s . K s m v) -> m v
> runK (K f) = f

> data S (s :: * -> *) = S
> newS :: (Monad m) => K s m (S (K s m))
> newS = return S

> class Up (a :: * -> *) (b :: * -> *) where
> up :: a v -> b v

> f :: (Up a b) => S a -> b ()
> f = undefined

Проблема заключается в написании инстансов для класса Up,
c Overlapping Instances такое реализуется использованием:


> instance Up a a where
> up = id

> instance Up a (K s a) where
> up = K

Банальное решение можно представить как:

> type family TQ (a :: * -> *) (b :: * -> *) :: Bool where
> TQ m1 (K s m2) = False
> TQ m m = True


> data Proxy (b::Bool) = Proxy

> class Up' (b::Bool) m1 m2 where
> up' :: Proxy b -> m1 a -> m2 a

> instance (Up' (TQ m1 m2) m1 m2) => Up m1 m2 where
> up = up' (Proxy::Proxy (TQ m1 m2))

> instance (m1 ~ m2) => Up' True m1 m2 where
> up' _ = id

> instance (Up m1 m2')
> => Up' False m1 (K s m2') where
> up' _ = K . up

Однако на самом деле оно не будет работать для некоторых примеров, например:

> example :: K s IO ()
> example = do
> x <- newS
> runK $ f x

причина этого заключается в том, что при проверке того, что тип является
"apart from" типа в правиле семейства типов допускаются бесконечные типы,
поэтому правило m1 (K s m2) не может быть отброшено даже при m m.
По всему этому делу есть небольшая дискуссия на trac [1]. При использовании
некоторой магии можно заставить работать не-полиморфный по стеку код как
в примере выше, но с полиморным (example :: Monad m => K s m ()) возникают
проблемы.

Поэтому у меня вопрос, может кто видит как это решить, или в данном случае
closed type families никак не могут помочь от использования
OverlappingInstances?


[1] https://ghc.haskell.org/trac/ghc/ticket/9918

--
Alexander