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
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
