Manuel said earlier that the source of the problem here is foo's
ambiguous type signature
(I'm switching back to the original, simplified example).
Type checking with ambiguous type signatures is hard because the type
checker has to guess
types and this guessing step may lead to too many (ambiguous) choices.
But this doesn't mean
that this worst case scenario always happens.
Consider your example again
type family Id a
type instance Id Int = Int
foo :: Id a -> Id a
foo = id
foo' :: Id a -> Id a
foo' = foo
The type checking problem for foo' boils down to verifying the formula
forall a. exists b. Id a ~ Id b
Of course for any a we can pick b=a to make the type equation statement
hold.
Fairly easy here but the point is that the GHC type checker doesn't do
any guessing
at all. The only option you have (at the moment, there's still lots of
room for improving
GHC's type checking process) is to provide some hints, for example mimicking
System F style type application by introducing a type proxy argument in
combination
with lexically scoped type variables.
foo :: a -> Id a -> Id a
foo _ = id
foo' :: Id a -> Id a
foo' = foo (undefined :: a)
Martin
Ganesh Sittampalam wrote:
On Wed, 9 Apr 2008, Manuel M T Chakravarty wrote:
Sittampalam, Ganesh:
No, I meant can't it derive that equality when matching (Id a)
against (Id b)? As you say, it can't derive (a ~ b) at that point,
but (Id a ~ Id b) is known, surely?
No, it is not know. Why do you think it is?
Well, if the types of foo and foo' were forall a . a -> a and forall b
. b -> b, I would expect the type-checker to unify a and b in the
argument position and then discover that this equality made the result
position unify too. So why can't the same happen but with Id a and Id
b instead?
The problem is really with foo and its signature, not with any use of
foo. The function foo is (due to its type) unusable. Can't you
change foo?
Here's a cut-down version of my real code. The type family Apply is
very important because it allows me to write class instances for
things that might be its first parameter, like Id and Comp SqlExpr
Maybe, without paying the syntactic overhead of forcing client code to
use Id/unId and Comp/unComp. It also squishes nested Maybes which is
important to my application (since SQL doesn't have them).
castNum is the simplest example of a general problem - the whole point
is to allow clients to write code that is overloaded over the first
parameter to Apply using primitives like castNum. I'm not really sure
how I could get away from the ambiguity problem, given that desire.
Cheers,
Ganesh
{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances,
NoMonomorphismRestriction #-}
newtype Id a = Id { unId :: a }
newtype Comp f g x = Comp { unComp :: f (g x) }
type family Apply (f :: * -> *) a
type instance Apply Id a = a
type instance Apply (Comp f g) a = Apply f (Apply g a)
type instance Apply SqlExpr a = SqlExpr a
type instance Apply Maybe Int = Maybe Int
type instance Apply Maybe Double = Maybe Double
type instance Apply Maybe (Maybe a) = Apply Maybe a
class DoubleToInt s where
castNum :: Apply s Double -> Apply s Int
instance DoubleToInt Id where
castNum = round
instance DoubleToInt SqlExpr where
castNum = SECastNum
data SqlExpr a where
SECastNum :: SqlExpr Double -> SqlExpr Int
castNum' :: (DoubleToInt s) => Apply s Double -> Apply s Int
castNum' = castNum
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
