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