Type Polymorphisme de famille

Question

J'ai donc une fonction apply :: proxy tf -> tf Int -> tf Int qui prend un proxy destiné à porter une famille de types et applique Int à cette famille de types pour déterminer le type du second argument et la valeur de retour. Cependant, je reçois des réponses confuses de GHC.

{-# LANGUAGE TypeFamilies #-} 

import Data.Proxy 

type family F (a :: *) :: * where 
    F Int =() 

f :: Proxy F 
f = Proxy 

apply :: proxy tf -> tf Int -> tf Int 
apply _ x = x 

-- Doesn't typecheck. 
test1 ::() 
test1 = apply f() 

-- Typechecks fine 
test2 ::() 
test2 = let g = apply f in g() 

test1 refuse de compiler avec GHC crachant cette erreur:

tftest.hs:16:9: 
    Couldn't match expected type ‘()’ with actual type ‘F Int’ 
    In the expression: apply f() 
    In an equation for ‘test1’: test1 = apply f() 

tftest.hs:16:17: 
    Couldn't match expected type ‘F Int’ with actual type ‘()’ 
    In the second argument of ‘apply’, namely ‘()’ 
    In the expression: apply f() 

Embrouillant, commentant test1 et en utilisant une liaison let dans test2 rend GHC heureux et tout compile bien. Quelqu'un peut-il expliquer ce qui se passe ici?

Answer 1

So I have a function apply :: proxy tf -> tf Int -> tf Int which takes a Proxy intended to carry a type family

Vous ne pouvez pas faire cela. Les familles de types doivent toujours être entièrement appliquées, comme les synonymes de type dont elles sont une généralisation. Une variable de type ne peut jamais être instanciée dans une famille de types sous-saturés.

C'est un bogue dans GHC 7.8.3 qu'il n'a pas déjà rejeté votre programme à partir de

f :: Proxy F