Ian Milligan | 14 Aug 02:02 2014
Picon

Closed Type Family Simplification

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
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 14 Aug 03:54 2014

Re: Closed Type Family Simplification

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 <ianmllgn <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
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
Ian Milligan | 14 Aug 04:42 2014
Picon

Re: Closed Type Family Simplification

Here is a small example which shows the problem

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module TypeFamilyTest where

import GHC.Prim

type family A ∷ * → Constraint

type family C f g a where C f g a = f (g a)

a ∷ A (f (g a)) ⇒ ()
a = ()

b ∷ A (C f g a) ⇒ ()
b = a


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
Ian Milligan | 14 Aug 04:54 2014
Picon

Re: Closed Type Family Simplification

Actually, that example is not quite right. Let me try to come up with another one.

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
Ian Milligan | 14 Aug 05:39 2014
Picon

Re: Closed Type Family Simplification

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
Ian Milligan | 14 Aug 05:48 2014
Picon

Re: Closed Type Family Simplification

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
Erik Hesselink | 14 Aug 11:17 2014
Picon

Re: Closed Type Family Simplification

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
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 14 Aug 13:42 2014

Re: Closed Type Family Simplification

Erik's analysis agrees with mine: type families can never be partially applied, and the fact that Ian's
latest example is accepted  as a syntactically correct program is a straightforward bug in GHC. If you try
that code on GHC 7.8.2, it will fail.

Type families can *never* be partially applied. (Data families are another story, though...)

Richard

On Aug 14, 2014, at 5:17 AM, Erik Hesselink <hesselink <at> gmail.com> wrote:

> 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
>> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe <at> haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 

Gmane