Data Union fs x where Here :: f

x -> Union (f : fs) x
There :: Union fs x -> Union (f : fs) x

class Remove f fs gs | f fs -> gs where
remove :: Union fs x -> Either (f x) (Union gs x)

instance {-# OVERLAPS #-} Remove f (f : fs) fs where
remove = union Left Right

instance Remove f fs gs => Remove f (g : fs) (g : gs) where
remove = union (Right . Elem) (fmap There . remove)

handle
:: forall f fs gs a x
. (Remove f fs gs)
=> (f x -> a)
-> (Union gs x -> a)
-> Union fs x -> a
handle handler rest = either handler rest . remove

type A = Union [[], Maybe, Identity] Int
type B = Union [Identity, [], Maybe] Int

foo :: A -> B
foo = handle @Maybe do _
$ _

Глядя на этот код, GHC заявляет:

• Found hole: _rest :: Union '[[], Maybe] Int -> B
• Found hole: _handler :: Maybe Int -> B
• Couldn't match type ‘Identity’ with ‘Maybe’
arising from a functional dependency between:
constraint ‘Remove Maybe '[Maybe, Identity] '[Maybe]’
arising from a use of ‘handle’
instance ‘Remove f (f : fs) fs’

Ни у кого, случайно, не завалялось под рукой выхода из этой ситуации?

что именно?

Для начала, GHC откуда-то откопал Remove Maybe '[Maybe, Identity] '[Maybe], которое не соответствует ни одному инстансу. Я пытался сделать gs зависимой переменной, но у GHC начинаются проблемы как при фундепах, так и если просто вынести gs в семейство типов

а где union?

Хм, у меня такое чувство что в undecidableinstances+fundeps что-то очень сильно сломано. Минимизируя, вот в таком {-# LANGUAGE Haskell2010, DataKinds, TypeOperators, FlexibleContexts, FlexibleInstances, UndecidableInstances, FunctionalDependencies, StandaloneKindSignatures #-} module WTF where import Data.Kind import Data.Proxy type Delete :: Type -> [Type] -> [Type] -> Constraint class Delete val src dst | val src -> dst instance Delete val (val:src) src instance Delete val src dst => Delete val (oth:src) (oth:dst) data A data B data C del :: Delete A [A, B, C] x => Proxy x del = Proxy test1 :: Proxy [B, C] test1 = del test2 :: Proxy _ test2 = del test1 нормально тайпчекается, а test2 дает те же ошибки WTF.hs:35:16: error: • Found type wildcard ‘_’ standing for ‘'[A, C] :: [*]’ To use the inferred type, enable PartialTypeSignatures • In the first argument of ‘Proxy’, namely ‘_’ In the type ‘Proxy _’ In the type signature: test2 :: Proxy _ | 35 | test2 :: Proxy _ | ^ WTF.hs:36:9: error: • Couldn't match type ‘B’ with ‘A’ arising from a functional dependency between: constraint ‘Delete A '[A, B, C] '[A, C]’ arising from a use of ‘del’ instance ‘Delete val (val : src) src’ at WTF.hs:21:10-33 • In the expression: del In an equation for ‘test2’: test2 = del | 36 | test2 = del То есть гхц сначала сам же выводит дырку как [A, C], а потом справедливо говорит что это на самом деле должно быть [B, C]. Но то что test1 тайпчекается не менее странно, так как инстансы вроде бы должны вызывать functional dependency conflict, и тут по идее даже overlapping прагмы не должны помогать, а все "работает" даже без них. Если же добавить instance Delete val '[] '[] то нормально тайпчекается такое, хотя по фундепу там должен быть только один возможный тип test1 :: Proxy [B, C] test1 = del test2 :: Proxy [A, B, C] test2 = del Кмк звучит как баг. @slowpnir, будешь репортить?