Técnicas para rastrear restricciones
Este es el escenario: escribí un código con una firma de tipo y GHC se queja de que no pudo deducir x ~ y para algunos xy y. Por lo general, puedes descartar el GHC y simplemente agregar el isomorfismo a las restricciones de la función, pero esto es una mala idea por varias razones:
- No enfatiza la comprensión del código.
- Puede terminar con 5 restricciones donde una hubiera sido suficiente (por ejemplo, si las 5 están implícitas en una restricción específica más)
- Puede terminar con restricciones falsas si ha hecho algo mal o si GHC no es útil
Pasé varias horas luchando contra el caso 3. Estoy jugando con syntactic-2.0, y estaba tratando de definir una versión independiente del dominio share, similar a la versión definida en NanoFeldspar.hs.
Tuve esto:
{-# LANGUAGE GADTs, FlexibleContexts, TypeOperators #-}
import Data.Syntactic
-- Based on NanoFeldspar.hs
data Let a where
Let :: Let (a :-> (a -> b) :-> Full b)
share :: (Let :<: sup,
Domain a ~ sup,
Domain b ~ sup,
SyntacticN (a -> (a -> b) -> b) fi)
=> a -> (a -> b) -> a
share = sugarSym Let
y GHC could not deduce (Internal a) ~ (Internal b), que ciertamente no es lo que buscaba. Entonces, o había escrito algún código que no tenía intención (que requería la restricción), o GHC quería esa restricción debido a otras restricciones que había escrito.
Resulta que necesitaba agregar (Syntactic a, Syntactic b, Syntactic (a->b))a la lista de restricciones, ninguna de las cuales implica (Internal a) ~ (Internal b). Básicamente me topé con las restricciones correctas; Todavía no tengo una forma sistemática de encontrarlos.
Mis preguntas son:
- ¿Por qué GHC propuso esa restricción? En ninguna parte sintáctica hay una restricción
Internal a ~ Internal b, entonces, ¿de dónde sacó eso GHC? - En general, ¿qué técnicas se pueden utilizar para rastrear el origen de una restricción que GHC cree que necesita? Incluso para las restricciones que puedo descubrir por mí mismo, mi enfoque es esencialmente forzar el camino ofensivo escribiendo físicamente las restricciones recursivas. Este enfoque básicamente se adentra en una infinita madriguera de restricciones y es el método menos eficiente que puedo imaginar.
En primer lugar, su función tiene el tipo incorrecto; Estoy bastante seguro de que debería serlo (sin el contexto) a -> (a -> b) -> b. GHC 7.10 es algo más útil al señalar esto, porque con su código original, se queja de una restricción faltante
Internal (a -> b) ~ (Internal a -> Internal a). Después de corregir shareel tipo, GHC 7.10 sigue siendo útil para guiarnos:
Could not deduce (Internal (a -> b) ~ (Internal a -> Internal b))Después de sumar lo anterior, obtenemos
Could not deduce (sup ~ Domain (a -> b))Después de sumar eso, obtenemos
Could not deduce (Syntactic a),Could not deduce (Syntactic b)yCould not deduce (Syntactic (a -> b))Después de agregar estos tres, finalmente verifica el tipo; entonces terminamos con
share :: (Let :<: sup, Domain a ~ sup, Domain b ~ sup, Domain (a -> b) ~ sup, Internal (a -> b) ~ (Internal a -> Internal b), Syntactic a, Syntactic b, Syntactic (a -> b), SyntacticN (a -> (a -> b) -> b) fi) => a -> (a -> b) -> b share = sugarSym Let
Entonces yo diría que GHC no ha sido inútil a la hora de guiarnos.
En cuanto a su pregunta sobre cómo rastrear de dónde obtiene GHC sus requisitos de restricción, puede probar los indicadores de depuración de GHC , en particular, -ddump-tc-tracey luego leer el registro resultante para ver dónde se agregan Internal (a -> b) ~ ty (Internal a -> Internal a) ~ tal Wantedconjunto, pero será una lectura bastante larga. .
¿Probaste esto en GHC 8.8+?
share :: (Let :<: sup,
Domain a ~ sup,
Domain b ~ sup,
SyntacticN (a -> (a -> b) -> b) fi,
_)
=> a -> (a -> b) -> a
share = sugarSym Let
La clave es utilizar el tipo agujero entre las restricciones:_ => your difficult type
