Allowing Instances to Unify Types

[Matt Brown]

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
<simonpj at microsoft.com> 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: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
> |  bounces at haskell.org] 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
> |  Glasgow-haskell-users at haskell.org
> |  http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>