Equality constraint type mismatch

[Isaac Dupree]

Subtree is a type-indexed family of type synonyms, in its first 
type-argument.  It cannot unify with 't :: * -> * -> *', because t must 
be a concrete type-constructor (not indexed, and perhaps not a normal 
type-synonym either).

Delayed (t Pure)
~
t Lazy

lets us conclude
Delayed ~ t ; (t Pure) ~ Lazy
and then
(Delayed Pure) ~ Lazy
which I'm sure you can see is not true. This happens because 't' cannot 
be chosen to be something like 'Subtree', only something like 'Arrow'. 
(in fact there's a kind mismatch above, in Delayed ~ t, so the conflict 
happens even sooner)

However

Delayed (Subtree Pure)
~
Subtree Lazy

simplifies to (because we can resolve Subtree, because its argument is 
given concretely in each case)

Delayed Tree
~
Delayed Tree

which is obviously a tautology.

-Isaac


On 03/07/10 12:41, C Rodrigues wrote:
>
> I would like help understanding a type error I'm getting with GHC 6.10.4.
> GHC reports a type mismatch for the types in a satisfiable equality
> constraint.  The function "idLazy" below demonstrates the error.  I would
> appreciate if someone can explain what's going on.
>
> Thanks,
> -heatsink
>
> {-# LANGUAGE TypeFamilies, EmptyDataDecls, ScopedTypeVariables, FlexibleContexts #-}
> module Test where
>
> import Control.Monad
>
> -- These types are used as type indices
> data Pure
> data Lazy
>
> -- Delayed evaluation in the IO monad
> data Delayed t a = Delayed (IO (t a))
>
> {- This function definition gives me the error
> Test.hs:24:0:
>      Couldn't match expected type `Delayed (t Pure)'
>             against inferred type `t Lazy'
> But that's exactly what my constraint says!  What's wrong?
> -}
> idLazy :: forall (t :: * ->  * ->  *). t Lazy ~ Delayed (t Pure) =>
>            Delayed (t Pure) Lazy ->  Delayed (t Pure) Lazy
> idLazy x = x
>
>
> -- Below, I provide an instance of 't' that makes idLazy well-typed.
> -- A type-indexed data structure
> data Tree a = Leaf Int | Branch (Subtree a a) (Subtree a a)
>
> -- The first parameter to 'Subtree' determines what type the outermost
> -- constructor will have.  The second parameter determines what type
> -- the inner constructors will have.
> type family Subtree a :: * ->  *
>
> -- Two instances of the data structure
> type instance Subtree Pure = Tree
> type instance Subtree Lazy = Delayed Tree
> {- If I use this type signature, there is no error
> idLazy :: Subtree Lazy ~ Delayed (Subtree Pure) =>
>            Delayed (Subtree Pure) Lazy ->  Delayed (Subtree Pure) Lazy
> -}
>   		 	   		
> _________________________________________________________________
> Hotmail: Trusted email with powerful SPAM protection.
> http://clk.atdmt.com/GBL/go/201469227/direct/01/_______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>