Simon and Thomas, By instance unifs, I mean instances that do not match, but do "unify", although I'm not entirely clear on what that means. My current thinking is "could match, given some additional type information, such as equality predicates". I refer to them as unifs, because that is how they're labelled in the "lookupInst fail" message from -ddump-tc-trace.
I've been toying with several ideas of dubious practicality, primarily as a way to explore the inner workings of GHC (which has been great fun btw). In this case, before TcSimplify.checkLoop exits, if irreds is not null, reduceContext is run again with a flag that tells lookupPred to accept an "instance unif", when a sensible choice can be made (for example, when there is only one possible choice). This is my limited understanding of the issue: The expression: print `applyInst` (return "bar") Contains three constraints: Show a, Monad m, and Apply (a -> IO ()) (m [Char]) (IO b) Where the Show predicate is required by print, Monad by return, and Apply by applyInst. With my modifications, the lookup for the Apply predicate yields: Apply ([Char] -> IO ()) (IO [Char]) (IO ()) Which implies two equality constraints (a ~ [Char], m ~ IO). Knowing that, I'd like to be able to resolve (Show a, Monad m) as (Show [Char], Monad IO). Put more simply, I'd like the applyInst expression to typecheck as the apply expression does. Reading through the OutsideIn paper over the weekend, I began to understand why it isn't so simple. I'm looking forward to furthering my understanding, and continuing my experiments with the new typechecker. Thank you both for the informative responses, -matt On Mon, Jul 26, 2010 at 3:11 AM, Simon Peyton-Jones <[email protected]> wrote: > Matt > > I afraid I didn't understand your email well enough to offer a coherent > response. For example I have no clue what "instance unifs" might mean. Nor > do I understand what your program seeks to achieve. > > Thomas is right to say that the type checker is in upheaval at the moment. > I'm actively working on it with Dimitrios > (http://darcs.haskell.org/ghc-new-tc/ghc for the over-interested), but it'll > be a month or two before it gets into HEAD. However the plan is to do so for > the 6.14 release. > > Simon > > | -----Original Message----- > | From: [email protected] > [mailto:glasgow-haskell-users- > | [email protected]] On Behalf Of Matt Brown > | Sent: 23 July 2010 21:47 > | To: glasgow-haskell-users > | Subject: Allowing Instances to Unify Types > | > | Hi all, > | I've been hacking on GHC for a couple months now, experimenting with > | some different ideas I find interesting. One thing I'm trying to do > | is allow instance unifs (when there's an unambiguous choice, a > | question which is simplified in this case by there being only one), > | and force the required unification. Here's a simple example: > | > | {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, > | FlexibleInstances, UndecidableInstances #-} > | class Apply a b c | a b -> c where > | applyInst :: a -> b -> c > | > | instance (Monad m) => Apply (a -> m b) (m a) (m b) where > | applyInst = (=<<) > | > | apply :: (Monad m) => (a -> m b) -> (m a) -> (m b) > | apply = (=<<) > | > | ioStr :: IO String > | ioStr = return "foo" > | > | printStr :: String -> IO () > | printStr = print > | > | main = do print `apply` (return "foo") > | printStr `applyInst` ioStr > | print `applyInst` (return "bar") -- this fails > | > | > | With my code to use the unif instance enabled, I get Ambiguous type > | variable errors for "Show a" (from print) and "Monad m" (from return). > | > | My question is: in the case of apply (which isn't implemented by a > | class), how does the typechecker propagate "a ~ String" and "m ~ IO" > | to the predicates for print and return? If someone (such as myself) > | had sufficient time and energy to spend trying to achieve similar > | behavior for applyInst, where might he/I start? > | > | Thanks and Regards, > | -matt > | _______________________________________________ > | 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
