Hi,

I've been working on a kind of constrained version of Data.Dynamic:

	data Dynamic (c :: * -> Constraint) where
	    Dynamic :: (Typeable a, c a) => a -> Dynamic c

The idea is that Data.Dynamic gives up all compile time type information. In this variant I can at least keep a bit of the information around that I have. (In fact I can even "lift" a type into a constraint, thereby keeping all information.) Most of my functions are nailed down, including mappings and traversals. But one group of functions eludes me: functions to change only the constraint, while keeping the value. Here is one of my goal types:

	castDynamic :: ( Typeable a, c a, d a ) => Dynamic c -> Dynamic d

I'm pretty sure I'll have to sprinkle in a Proxy a, but so be it. I've thrown all typing tricks at this function that I know of, from unsafeCoerce over case-of instead of pattern matching, to ScopedTypeVariables. But I couldn't convince ghci to accept my code. So I tried something simpler.

	castDynamic' :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)

Here's where it gets funny: I can implement this function in ghci interactively just fine.

	>>> :t \(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a
	\(d :: Dynamic Show) -> case d of Dynamic a -> Dynamic <$> cast a
	  :: (Typeable a, c a) => Dynamic Show -> Maybe (Dynamic c)

But when I enter the exact same code in a file and load it, ghci balks at me because a is too ambiguous. Again, I've tried if it's the monomorphism restriction, or if I need to sprinkle in more (scoped) signatures or explicit forall's etc… nothing helped.

What is the difference here? Am I missing an extension? Am I doing something I shouldn't and the interactive mode is just doing me a favor? There was a discussion on this list less than a month ago where it was mentioned that ghci handles polymorphic types differently depending on the source of the code. Is there some documentation on these differences? Any help would be appreciated.

Cheers,
MarLinn