Convert type-level list '[a,b,c,...] to function a->b->c->

Question

I have a data family indexed by type-level list, where types in a list correspond to parameters of a data instance. I want to write function that will have different arity and parameters depending on a data instance, so I could use it like synonym for every data instance in the family.

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
             TypeFamilies, FlexibleInstances, PolyKinds #-}

module Issue where


type family (->>) (l :: [*]) (y :: *) :: * where
    '[]       ->> y = y
    (x ': xs) ->> y = x -> (xs ->> y)

class CVal (f :: [*]) where
    data Val f :: *
    construct :: f ->> Val f

instance CVal '[Int, Float, Bool] where
    data Val '[Int, Float, Bool] = Val2 Int Float Bool
    construct = Val2

This compiles fine. But when I try to apply construct function:

v :: Val '[Int, Float, Bool]
v = construct 0 0 True

it produces error:

Couldn't match expected type `a0
                              -> a1 -> Bool -> Val '[Int, Float, Bool]'
            with actual type `f0 ->> Val f0'
The type variables `f0', `a0', `a1' are ambiguous
The function `construct' is applied to three arguments,
but its type `f0 ->> Val f0' has none
In the expression: construct 0 0 True
In an equation for `v': v = construct 0 0 True

Cactus Cactus · Accepted Answer · 2015-07-01T07:33:56

Your code fails to typecheck because type families are not (necessarily) injective. If you help out GHC by specifying the choice of f in f ->> Val f, then it works as expected:

{-# LANGUAGE KindSignatures, DataKinds, TypeOperators, 
             TypeFamilies, FlexibleInstances, PolyKinds #-}

module Issue where

import Data.Proxy

type family (->>) (l :: [*]) (y :: *) :: * where
    '[]       ->> y = y
    (x ': xs) ->> y = x -> (xs ->> y)

class CVal (f :: [*]) where
    data Val f :: *
    construct :: proxy f -> f ->> Val f

instance CVal '[Int, Float, Bool] where
    data Val '[Int, Float, Bool] = Val2 Int Float Bool deriving Show
    construct _ = Val2

v :: Val '[Int, Float, Bool]
v = construct (Proxy :: Proxy '[Int, Float, Bool]) 0 0 True

The key point is passing that Proxy :: Proxy '[Int, Float, Bool] argument to construct, thereby fixing the choice of f. That is because there is nothing holding you back from having types f1 and f2 such that f1 ->> Val f1 ~ f2 ->> Val f2.

Don't worry, this shortcoming of the language is being looked at.

Convert type-level list '[a,b,c,...] to function a->b->c->

1 Answers