[Haskell-cafe] Closed Type Family Simplification

[Ian Milligan]

This is enough to demonstrate this error:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

module TypeFamilyTest where

type family B f g a where B f g a = f (g a)
newtype C f a = C (f a)
t :: (forall a. a -> f a) -> (forall a. a -> g a) -> a -> C (B f g) a
t f g a = C (f (g a))

Is it not possible to use type families in this way?

On Wednesday, August 13, 2014 8:39:09 PM UTC-7, Ian Milligan wrote:
>
> I suspect the problem happens because I am trying to use a partially 
> applied type family with a type constructor. However, in trying to 
> replicate the problem I ran into another strange error message with the 
> following program (using tagged and constraints as I was trying to keep it 
> as close to the original program as possible)
>
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE ConstraintKinds #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE TypeOperators #-}
>
> module TypeFamilyTest where
>
> import GHC.Prim
> import Data.Constraint
> import Data.Tagged
> import Data.Proxy
>
> type family A :: * -> Constraint
> type family B f g a where B f g a = f (g a)
> newtype C f = C (forall a. Tagged a (A a :- A (f a)))
>
> t :: forall f g a. C f -> C g -> C (B f g)
> t (C x) (C y) = C z where
>     z :: forall a. Tagged a (A a :- A (f (g a)))
>     z = Tagged (trans (proxy x (Proxy :: Proxy (g a))) (proxy y (Proxy :: 
> Proxy a)))
>
> This fails with the error message
>
> TypeFamilyTest.hs:21:19:
>     Couldn't match type ‘a1’ with ‘g a1’
>       ‘a1’ is a rigid type variable bound by
>            a type expected by the context: Tagged a1 (A a1 :- A (f a1))
>            at TypeFamilyTest.hs:21:17
>     Expected type: Tagged a1 (A a1 :- A (f a1))
>       Actual type: Tagged a1 (A a1 :- A (f (g a1)))
>     Relevant bindings include
>       z :: forall a. Tagged a (A a :- A (f (g a)))
>         (bound at TypeFamilyTest.hs:23:5)
>       y :: forall a. Tagged a (A a :- A (g a))
>         (bound at TypeFamilyTest.hs:21:12)
>       t :: C f -> C g -> C (B f g) (bound at TypeFamilyTest.hs:21:1)
>     In the first argument of ‘C’, namely ‘z’
>     In the expression: C z
>
> for some reason C (B f g) expects Tagged a1 (A a1 :- A (f a1)) instead of 
> Tagged a1 (A a1 :- A (f (g a1)))?
>
> On Wednesday, August 13, 2014 6:54:45 PM UTC-7, Richard Eisenberg wrote:
>>
>> Your operating assumption sounds right. Do you have a complete, minimal 
>> example showing the error? If not, I recommend using -fprint-explicit-kinds 
>> to see if kinds are getting in your way at all. 
>>
>> Richard 
>>
>> On Aug 13, 2014, at 8:02 PM, Ian Milligan <ianm... at gmail.com> wrote: 
>>
>> > When a closed type family has only one instance it seems like it should 
>> never fail to simplify. Yet this doesn't appear to be the case. When I 
>> defined (in GHC 7.8.3) the closed type family 
>> > type family (:.:) f g a where (:.:) f g a = f (g a) 
>> > I get errors such as 
>> > 'Could not deduce (Object c3 ((:.:) f g a) ~ Object c3 (f (g a)))' 
>> > (where Object is a Constraint family), indicating that f (g a) is not 
>> being substituted for (:.:) f g a as desired. Any idea why this happens? 
>> > _______________________________________________ 
>> > Haskell-Cafe mailing list 
>> > Haskel... at haskell.org 
>> > http://www.haskell.org/mailman/listinfo/haskell-cafe 
>>
>> _______________________________________________ 
>> Haskell-Cafe mailing list 
>> Haskel... at haskell.org 
>> http://www.haskell.org/mailman/listinfo/haskell-cafe 
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140813/fe7b90ef/attachment.html>