[Haskell-cafe] Closed Type Family Simplification

[Erik Hesselink]

I think partially applied type synonyms (and type families) are
supposed to be disallowed, but I recently found out that since GHC
7.8, this is not the case anymore, but you get very weird other type
errors instead. I filed a bug [0], perhaps yours is a similar issue.

Erik

[0] https://ghc.haskell.org/trac/ghc/ticket/9433#ticket

On Thu, Aug 14, 2014 at 5:48 AM, Ian Milligan <ianmllgn at gmail.com> wrote:
> 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
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>