Changes between Initial Version and Version 1 of Ticket #927


Ignore:
Timestamp:
Oct 9, 2006 8:06:32 AM (8 years ago)
Author:
simonpj
Comment:

The monomorphism restriction (which foo falls under) says that "the constrained type variables of a restricted group are not generalised". But it's very hard to say just what the "constrainted variables" are. Not the ones that appear in the constraint -- because simplifying the constraint might eliminate them. So perhpas we should simplify the constraint first, and see what is free?

Should we use improvement during simplification? Presumably -- but that elicited a bug that I documented but cannot now remember. I give the comment and the code it refers to below. So GHC currently *does* simplify but *does not* use improvement, when trying to figure out which variables to generalise.

As a result, it does not generalise 'a' in your example, and then (since 'a' is monomorphic) it is squashed to ().

My take on this is that we should simplify the monomorphism restriction: either the binding is fully polymorphic or fully monomorphic. The business of figuring out what the "constrainted variables" are is just too subtle.

Comments from the code:

tcSimplifyRestricted infers which type variables to quantify for a 
group of restricted bindings.  This isn't trivial.

Eg1:	id = \x -> x
	We want to quantify over a to get id :: forall a. a->a
	
Eg2:	eq = (==)
	We do not want to quantify over a, because there's an Eq a 
	constraint, so we get eq :: a->a->Bool	(notice no forall)

So, assume:
	RHS has type 'tau', whose free tyvars are tau_tvs
	RHS has constraints 'wanteds'

Plan A (simple)
  Quantify over (tau_tvs \ ftvs(wanteds))
  This is bad. The constraints may contain (Monad (ST s))
  where we have 	instance Monad (ST s) where...
  so there's no need to be monomorphic in s!

  Also the constraint might be a method constraint,
  whose type mentions a perfectly innocent tyvar:
	  op :: Num a => a -> b -> a
  Here, b is unconstrained.  A good example would be
	foo = op (3::Int)
  We want to infer the polymorphic type
	foo :: forall b. b -> b


Plan B (cunning, used for a long time up to and including GHC 6.2)
  Step 1: Simplify the constraints as much as possible (to deal 
  with Plan A's problem).  Then set
	qtvs = tau_tvs \ ftvs( simplify( wanteds ) )

  Step 2: Now simplify again, treating the constraint as 'free' if 
  it does not mention qtvs, and trying to reduce it otherwise.
  The reasons for this is to maximise sharing.

  This fails for a very subtle reason.  Suppose that in the Step 2
  a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
  In the Step 1 this constraint might have been simplified, perhaps to
  (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
  This won't happen in Step 2... but that in turn might prevent some other
  constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) 
  and that in turn breaks the invariant that no constraints are quantified over.

  Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
  the problem.


Plan C (brutal)
  Step 1: Simplify the constraints as much as possible (to deal 
  with Plan A's problem).  Then set
	qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
  Return the bindings from Step 1.
  

A note about Plan C (arising from "bug" reported by George Russel March 2004)
Consider this:

      instance (HasBinary ty IO) => HasCodedValue ty

      foo :: HasCodedValue a => String -> IO a

      doDecodeIO :: HasCodedValue a => () -> () -> IO a
      doDecodeIO codedValue view  
        = let { act = foo "foo" } in  act

You might think this should work becuase the call to foo gives rise to a constraint
(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO.  But the
restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
constraint using the (rather bogus) instance declaration, and now we are stuffed.

I claim this is not really a bug -- but it bit Sergey as well as George.  So here's
plan D


Plan D (a variant of plan B)
  Step 1: Simplify the constraints as much as possible (to deal 
  with Plan A's problem), BUT DO NO IMPROVEMENT.  Then set
	qtvs = tau_tvs \ ftvs( simplify( wanteds ) )

  Step 2: Now simplify again, treating the constraint as 'free' if 
  it does not mention qtvs, and trying to reduce it otherwise.

  The point here is that it's generally OK to have too few qtvs; that is,
  to make the thing more monomorphic than it could be.  We don't want to
  do that in the common cases, but in wierd cases it's ok: the programmer
  can always add a signature.  

  Too few qtvs => too many wanteds, which is what happens if you do less
  improvement.

The example tc177

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}

-- This is a rather complicated program that uses functional 
-- dependencies to do Peano arithmetic.
--
-- GHC 6.2 dies because tcSimplifyRestricted was trying to
-- be too clever.  See 'Plan B' in tcSimplifyRestricted

module ShouldCompile where



-- This is the offending definition.  It falls under
-- the monomorphism restriction, so tcSimplifyRestricted applies
bug = ins b (ins b Nil)


------------------------------------
data LAB l r = LAB l r deriving Show

data OR a b = OR a b deriving Show


data Cons x y = Cons x y deriving Show

data Nil = Nil deriving Show

data T = T

data F = F

data A = A deriving Show

data B = B deriving Show

data Zero = Zero

data Succ n = Succ n

b = ((LAB B []),[])

-- insertion function
-- insert label pairs in the a list of list, each list contains a collection of
-- label pair that sharing the common label.


class Ins r l l' | r l -> l' where
    ins :: r -> l -> l'


instance Ins ((LAB l1 r1),r1') Nil (Cons (Cons ((LAB l1 r1),r1') Nil) Nil) where
    ins l Nil = (Cons (Cons l Nil) Nil)
   

instance ( L2N l1 n1
     , L2N l2 n2
     , EqR n1 n2 b
     , Ins1 ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') b l
     ) => Ins ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') l 
    where
      ins ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') 
	= ins1  ((LAB l1 r1),r1') (Cons (Cons ((LAB l2 r2),r2') rs) rs') 
		(eqR (l2n l1)  (l2n l2))
-- Note that n1 and n2 are functionally defined by l1 and l2, respectively,
-- and b is functionally defined by n1 and n2.


class Ins1 r l b l' | r l b -> l' where
    ins1 :: r -> l -> b -> l'

instance Ins1 ((LAB l1 r1),r1') (Cons r rs) T 
	      (Cons (Cons ((LAB l1 r1),r1') r) rs) where
   ins1 l (Cons r rs) _ = (Cons (Cons l r) rs)

instance ( Ins ((LAB l1 r1),r1') rs rs') 
      => Ins1 ((LAB l1 r1),r1') (Cons r rs) F (Cons r rs') where
    ins1 l (Cons r rs) _ = (Cons r (ins l rs))

-- class for mapping label to number

class L2N l n | l -> n where
    l2n :: l -> n

instance L2N A Zero where
    l2n A = Zero

instance L2N B (Succ Zero) where
    l2n B = Succ Zero


-- class for comparing number type

class EqR n1 n2 b | n1 n2 -> b where
    eqR :: n1 -> n2 -> b

instance EqR Zero Zero T where
    eqR _ _ = T

instance EqR Zero (Succ n) F where
    eqR _ _ = F

instance EqR (Succ n) Zero F where
    eqR _ _ = F

instance (EqR n1 n2 b) => EqR (Succ n1) (Succ n2) b where
    eqR (Succ n1) (Succ n2) = eqR n1 n2

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #927 – Description

    initial v1  
    11A small module loaded into ghci -fglasgow-exts 6.4.1: 
    2  
     2{{{ 
    33module M where 
    44 
     
    1515 
    1616foo :: () -> () 
    17  
    18 I would expect a -> () -- what gives? 
     17}}} 
     18I would expect `a -> ()` -- what gives? 
    1919 
    2020John Hughes