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...@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...@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