GHC: Ticket #3043: An unrelated definition monomorphizes a type even without the MR
http://ghc.haskell.org/trac/ghc/ticket/3043
<p>
The following code:
</p>
<pre class="wiki">{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}
class Id a b | b -> a where id' :: a -> b
instance Id [Char] [Char] where id' = id
class Fst a where fst' :: a -> String
instance Fst ([Char],a) where fst' = fst
data Void a = Void
void :: (String,a) -> Void a
void _ = Void
fst'' (a,b) =
let x = (id' a, b)
y = void x :: Void Int -- remove this line and the code compiles
in fst' x
</pre><p>
Results in:
</p>
<pre class="wiki">arst.hs:18:6:
No instance for (Fst (b, Int))
arising from a use of `fst'' at arst.hs:18:6-11
Possible fix: add an instance declaration for (Fst (b, Int))
In the expression: fst' x
In the expression:
let
x = (id' a, b)
y = void x :: Void Int
in fst' x
In the definition of `fst''':
fst'' (a, b)
= let
x = ...
y = ...
in fst' x
arst.hs:18:11:
No instance for (Id [Char] b)
arising from a use of `x' at arst.hs:18:11
Possible fix: add an instance declaration for (Id [Char] b)
In the first argument of `fst'', namely `x'
In the expression: fst' x
In the expression:
let
x = (id' a, b)
y = void x :: Void Int
in fst' x
</pre><p>
It seems that the definition of <code>y</code> locks down the type of <code>x</code> somewhat even though the monomorphism restriction is disabled. If we remove the definition:
</p>
<pre class="wiki">*Main> :t fst''
fst'' :: (Id t b, Fst (b, t1)) => (t, t1) -> String
</pre><p>
To be completely honest I'm not sure whether the code should be accepted or not, since <code>(Id t b, Fst (b, t1))</code> can't be satisfied. Only the fully monomorphic signature <code>([Char], Int) -> String</code>, which is obtained with the definition of <code>y</code> in place and the monomorphism restriction enabled, works.
</p>
<p>
In any case, I think it's a bug that the results of the type check depend on whether <code>y</code> is defined or not: surely that shouldn't matter at all, no matter what the end result is.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/3043
Trac 1.2simonpjMon, 23 Feb 2009 17:57:17 GMTstatus changed; difficulty, resolution set
http://ghc.haskell.org/trac/ghc/ticket/3043#comment:1
http://ghc.haskell.org/trac/ghc/ticket/3043#comment:1
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
Your final remark isn't right in general. Consider:
</p>
<pre class="wiki">f x = let y = x::Int
in x && True
</pre><p>
This is rejected, because <code>x</code> can't be both an <code>Int</code> and a <code>Bool</code>. But it'd be accepted if the binding for <code>y</code> was dropped. The type checker takes no notice of whether <code>y</code> is mentioned or not. (You might want it to, but I don't think it matters one way or the other in practice.)
</p>
<p>
In your example, since <code>a</code> and <code>b</code> are both mentioned in the right hand side of <code>x</code>, the type of <code>x</code> can't be generalised. Suppose <code>a :: ta</code> and <code>b :: tb</code>. Then the inferred type for <code>x</code> will be something like
</p>
<pre class="wiki"> x :: forall c. Id ta c => (c, tb)
</pre><p>
Now the type sig in <code>y</code> instantiates <code>c</code> to <code>String</code>, forces <code>tb=Int</code>, and generates a constraint <code>(Id ta String)</code>. Now the fundep on <code>Id</code> forces <code>ta=String</code>.
</p>
<p>
That's as far as I have time to go today. I don't think this has anything to do with the MR.
</p>
<p>
Reopen if you disagree.
</p>
<p>
Simon
</p>
Ticket