Equality constraint type mismatch
Isaac Dupree
ml at isaac.cedarswampstudios.org
Sun Mar 7 15:01:50 EST 2010
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
>
More information about the Glasgow-haskell-users
mailing list