Changes between Initial Version and Version 1 of Ticket #927
 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 fglasgowexts fallowundecidableinstances #}  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 1 1 A small module loaded into ghci fglasgowexts 6.4.1: 2 2 {{{ 3 3 module M where 4 4 … … 15 15 16 16 foo :: () > () 17 18 I would expect a > () what gives?17 }}} 18 I would expect `a > ()`  what gives? 19 19 20 20 John Hughes