[GHC] #927: Type checker infers () instead of a
GHC
trac at galois.com
Mon Oct 9 04:06:32 EDT 2006
#927: Type checker infers () instead of a
-----------------------+----------------------------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 6.4.1
Severity: normal | Resolution:
Keywords: | Os: Windows
Difficulty: Unknown | Architecture: x86
-----------------------+----------------------------------------------------
Old description:
> A small module loaded into ghci -fglasgow-exts 6.4.1:
>
> module M where
>
> class C a b | a -> b where
> same :: a -> b
>
> instance C () ()
>
> instance C a b => C (c -> a) (c -> b)
>
> foo = same (const ())
>
> Asking :i foo yields
>
> foo :: () -> ()
>
> I would expect a -> () -- what gives?
>
> John Hughes
New description:
A small module loaded into ghci -fglasgow-exts 6.4.1:
{{{
module M where
class C a b | a -> b where
same :: a -> b
instance C () ()
instance C a b => C (c -> a) (c -> b)
foo = same (const ())
Asking :i foo yields
foo :: () -> ()
}}}
I would expect `a -> ()` -- what gives?
John Hughes
Comment (by simonpj):
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
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/927>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the Glasgow-haskell-bugs
mailing list