Closed Type Family Simplification

Ian Milligan

13 Aug 2014 13 Aug '14

8:02 p.m.

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?

Attachments:

attachment.html (text/html — 523 bytes)

Show replies by date

Richard Eisenberg

13 Aug 13 Aug

9:54 p.m.

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 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Ian Milligan

10:42 p.m.

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 javascript:> 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...@haskell.org javascript: http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org javascript: http://www.haskell.org/mailman/listinfo/haskell-cafe

Ian Milligan

10:54 p.m.

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 javascript:> 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...@haskell.org javascript: http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org javascript: http://www.haskell.org/mailman/listinfo/haskell-cafe

Ian Milligan

11:39 p.m.

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 javascript:> 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...@haskell.org javascript: http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org javascript: http://www.haskell.org/mailman/listinfo/haskell-cafe

Ian Milligan

11:48 p.m.

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 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...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Erik Hesselink

14 Aug 14 Aug

5:17 a.m.

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 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 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...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Richard Eisenberg

7:42 a.m.

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 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 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 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...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskel...@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

3935

Age (days ago)

3935

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Erik Hesselink
Ian Milligan
Richard Eisenberg