¿Por qué TypeSynonymInstances no permite utilizar sinónimos de tipo aplicado parcialmente en los cabezales de instancia?

Question

Sé que TypeSynomymInstances only allows fully applied type synonyms to be used in instance heads, pero parece que sería útil si pudiera usar sinónimos de tipo aplicados parcialmente para ser utilizados también.

Por ejemplo:

class Example e where 
    thingy :: a -> b -> e a b 

-- legit, but awkward 
newtype FuncWrapper e a b = FuncWrapper { ap :: a -> e a b } 
instance (Example e) => Example (FuncWrapper e) where 
    thingy _ = FuncWrapper . flip thingy 
funcWrapperUse :: (Example e) => e Int String 
funcWrapperUse = thingy 1 "two" `ap` 3 `ap` 4 `ap` 5 

-- not legal, but a little easier to use 
type FuncSynonym e a b = a -> e a b 
instance (Example e) => Example (FuncSynonym e) where 
    thingy _ = flip thingy 
funcSynonymUse :: (Example e) => e Int String 
funcSynonymUse = thingy 1 "two" 3 4 5 

Answer 1

sinónimos tipo aplicadas parcialmente no están permitidos en Haskell en absoluto. Un sinónimo parcialmente aplicado es efectivamente una función cuyas entradas son los tipos no aplicados y cuyo resultado es un tipo. Por ejemplo, aquí es una codificación de lógica booleana:

type True x y = x 
type False x y = y 
type Not b x y = b y x 
type And b1 b2 x y = b1 (b2 x y) y 
type Or b1 b2 x y = b1 x (b2 x y) 

Para decidir si dos sinónimos tipo parcialmente aplicadas son iguales, el tipo de corrector tendrá que decidir si las funciones son iguales. Este es un problema difícil, y en general es indecidible.

Answer 2

Otro problema con permitir sinónimos de tipo aplicado parcialmente es que harían la inferencia de tipo y la selección de instancia esencialmente imposible. Por ejemplo, supongamos en el contexto de algún programa que quería usar thingy en el tipo Int -> String -> Int -> (Int, String). thingy tiene por tipo forall a b e. a -> b -> e a b, por lo que puede unificar a con Int y b con String, pero si e se le permite ser un sinónimo de tipo aplicado parcialmente, podríamos tener

e = FuncSynonym (,) 

o

e = FuncSynonym' Int (,) where type FuncSynonym' x f a b = x -> f a b 

o incluso

e = Const2 (Int -> (Int, String)) where Const2 a x y = a 

El problema del tipo inferencia sería incluso peor que decidir la igualdad de funciones; requeriría considerar todas las funciones con salida especificada en una entrada particular, o problemas similares más complicados (imagínese simplemente tratando de unificar a b con Int).