GHC: Ticket #1897: Ambiguous types and rejected type signatures
http://ghc.haskell.org/trac/ghc/ticket/1897
<p>
This ticket collects a bunch of examples where GHC
</p>
<ul><li>Rejects a function with a type signature but, if the type signature is removed, accepts the function and infers precisely the type that was originally specified.
</li><li>Accepts type signatures that are utterly ambiguous; that is, the function could never be called, or only in the presence of bizarre instance declarations.
</li><li>Rejects definitions that clearly have a unique typing.
</li></ul><p>
Original example: the following programm does not compile:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
import Control.Monad
import Data.Maybe
class Bug s where
type Depend s
next :: s -> Depend s -> Maybe s
start :: s
isValid :: (Bug s) => [Depend s] -> Bool
isValid ds = isJust $ foldM next start ds
</pre><p>
Error:
</p>
<pre class="wiki">GHCi, version 6.9.20071105: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( GHC-Bug.hs, interpreted )
Bug.hs:13:39:
Couldn't match expected type `Depend a'
against inferred type `Depend s'
Expected type: [Depend a]
Inferred type: [Depend s]
In the third argument of `foldM', namely `ds'
In the second argument of `($)', namely `foldM next start ds'
Failed, modules loaded: none.
</pre><p>
When one elides the type signature the program compiles yielding the offending signature:
</p>
<pre class="wiki">Prelude> :r
[1 of 1] Compiling Main ( GHC-Bug.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t isValid
isValid :: (Bug a) => [Depend a] -> Bool
</pre><p>
Compiler version: 6.9.20071105
</p>
<p>
Best regards,
</p>
<blockquote>
<p>
Harald Holtmann (haskell@…)
</p>
</blockquote>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/1897
Trac 1.0.1guestThu, 15 Nov 2007 11:07:09 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/1897
http://ghc.haskell.org/trac/ghc/ticket/1897
<ul>
<li><strong>attachment</strong>
set to <em>GHC-Bug.hs</em>
</li>
</ul>
TicketiglooSat, 17 Nov 2007 23:04:46 GMTcomponent changed; owner, difficulty, milestone set
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:1
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:1
<ul>
<li><strong>owner</strong>
set to <em>chak</em>
</li>
<li><strong>difficulty</strong>
set to <em>Unknown</em>
</li>
<li><strong>component</strong>
changed from <em>Compiler</em> to <em>Compiler (Type checker)</em>
</li>
<li><strong>milestone</strong>
set to <em>6.10 branch</em>
</li>
</ul>
<p>
Thanks for the report. Looks like one for you, Manuel.
</p>
TicketpgavinTue, 03 Jun 2008 00:04:12 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:2
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:2
<p>
just a note: it seems that the following thread may apply, in case someone else runs into this problem:
</p>
<p>
<a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2008-April/041397.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2008-April/041397.html</a>
</p>
TicketchakTue, 03 Jun 2008 07:56:44 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:3
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:3
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
This is not a bug, see the discussion in the mailing list URL of the previous comment.
</p>
TicketsimonpjTue, 03 Jun 2008 09:39:48 GMTpriority, status changed; resolution deleted
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:4
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:4
<ul>
<li><strong>priority</strong>
changed from <em>normal</em> to <em>low</em>
</li>
<li><strong>status</strong>
changed from <em>closed</em> to <em>reopened</em>
</li>
<li><strong>resolution</strong>
<em>invalid</em> deleted
</li>
</ul>
<p>
I think we should leave this open, albeit at low priority, because the error message is rather confusing. It's far from obvious how to improve it, but it's a nice example.
</p>
<p>
Simon
</p>
TicketIsaac DupreeTue, 03 Jun 2008 15:35:33 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:5
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:5
<p>
In this case I'd say something like "GHC can't figure out which class instance you mean by the function's arguments or results' types"... or let's see what an existing error says.
</p>
<pre class="wiki">foo :: (Show a, Read a) => Int
foo = 1 where x = show (read "xxx")
</pre><pre class="wiki">ambig.hs:4:0:
Ambiguous constraint `Show a'
At least one of the forall'd type variables mentioned by the constraint
must be reachable from the type after the '=>'
In the type signature for `foo':
foo :: (Show a, Read a) => Int
ambig.hs:4:0:
Ambiguous constraint `Read a'
At least one of the forall'd type variables mentioned by the constraint
must be reachable from the type after the '=>'
In the type signature for `foo':
foo :: (Show a, Read a) => Int
</pre><p>
Surely we can detect that? If there's something imprecise about "no use of the actual type variable" (outside non-FD class constraints and TF arguments)... See if the type unifies with a copy of itself, and if it doesn't, it shouldn't be allowed?
</p>
<p>
How about
</p>
<pre class="wiki"> Ambiguous constraint `Depend a'
At least one of the forall'd type variables mentioned by the constraint
must be reachable from the type after the '=>'
In the type signature for `isValid':
isValid :: (Bug s) => [Depend s] -> Bool
</pre><p>
Admittedly "reachable" might confuse people who don't think about what it means. It can be affected by equality constraints, for example. (is <tt>foo :: (a ~ Char, Show a, Read a) => Int; foo = 1</tt> supposed to be rejected by 6.9? It is rejected with the same "Ambiguous constraint" message... and is a useless type constraint, but not an ambiguous one per se) (but <tt>foo :: (a ~ Int) => F a -> F a; foo = id</tt> is perfectly fine) (Also, in this case, leaving <tt>foldM next start ds</tt> without a type-signature inside the type-information-losing <tt>isJust</tt>, ensures that <tt>isJust (foldM next start ds)</tt> has no usable type, for any <tt>ds</tt>.)
</p>
<p>
If we reject the explicit type signature of <tt>foo :: F a -> F a; foo = id</tt> in that thread outright, then I thought we're safe in assuming that this error will only appear in definitions that *do* have an explicit type-signature (it won't be inferred), unlike the typeclass one without its signature?:
</p>
<pre class="wiki">foo = 1 where x = show (read "xxx")
</pre><pre class="wiki">ambig.hs:5:24:
Ambiguous type variable `a' in the constraints:
`Read a' arising from a use of `read' at ambig.hs:5:24-33
`Show a' arising from a use of `show' at ambig.hs:5:18-34
Probable fix: add a type signature that fixes these type variable(s)
</pre><p>
But I might have been wrong: <tt>isJust (foldM next start ds)</tt> is just as bad as <tt>show . read</tt>: but then, I think that relies on it also having a typeclass constraint that's ambiguous, because you can introduce *that* without an explicit type-signature.
</p>
TicketsimonpjMon, 08 Sep 2008 15:09:22 GMTpriority changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:6
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:6
<ul>
<li><strong>priority</strong>
changed from <em>low</em> to <em>normal</em>
</li>
</ul>
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2157" title="feature request: Equality Constraints with Type Families (closed: fixed)">#2157</a> and <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2569" title="bug: Inferred type not accepted by compiler (closed: duplicate)">#2569</a>. And Ganesh's email <a class="ext-link" href="http://www.mail-archive.com/haskell-cafe@haskell.org/msg39593.html"><span class="icon"></span>http://www.mail-archive.com/haskell-cafe@haskell.org/msg39593.html</a>
</p>
<p>
We're now convinced that
</p>
<ul><li>There is really no good way to check the type of functions like <tt>isValid</tt>
</li><li>The right thing to do is to reject the type as ambiguous, whether it is inferred or checked. So the program would be rejected either way.
</li></ul><p>
Simon
</p>
TicketsimonpjTue, 09 Dec 2008 09:08:47 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:7
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:7
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2855" title="feature request: Surprising type (family) type derived (closed: duplicate)">#2855</a> (another instance of the same problem).
</p>
TicketsimonpjMon, 29 Dec 2008 16:30:26 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:8
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:8
<p>
See also <a class="ext-link" href="http://haskell.org/haskellwiki/GHC/Type_system#Type_signatures_and_ambiguity"><span class="icon"></span>http://haskell.org/haskellwiki/GHC/Type_system#Type_signatures_and_ambiguity</a> for an example unrelated to type functions.
</p>
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2885" title="bug: Late and confusing error on uncallable class method (closed: duplicate)">#2885</a> for yet another example.
</p>
<p>
We must sort out this ambiguity problem.
</p>
<p>
Simon
</p>
TicketsimonpjMon, 29 Dec 2008 16:35:24 GMTdescription, summary changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:9
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:9
<ul>
<li><strong>description</strong>
modified (<a href="/trac/ghc/ticket/1897?action=diff&version=9">diff</a>)
</li>
<li><strong>summary</strong>
changed from <em>Type families: type signature rejected</em> to <em>Ambiguous types and rejected type signatures</em>
</li>
</ul>
TicketsimonpjTue, 13 Jan 2009 11:49:48 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:10
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:10
<ul>
<li><strong>cc</strong>
<em>andres@…</em> added
</li>
</ul>
<p>
Here is yet another example, this time from Andres Loeh:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, EmptyDataDecls, RankNTypes #-}
module Foo where
data X (a :: *)
type family Y (a :: *)
-- This works (datatype).
i1 :: (forall a. X a) -> X Bool
i1 x = x
-- This works too (type family and extra arg).
i2 :: (forall a. a -> Y a) -> Y Bool
i2 x = x True
-- This doesn't work (type family).
i3 :: (forall a. Y a) -> Y Bool
i3 x = x
</pre><p>
The definition <tt>i3</tt> is currently rejected, because we can't determine that <tt>Y alpha ~ Y Bool</tt>, where <tt>alpha</tt> is an otherwise unconstrained unification variable, that comes from instantiating the occurrence of <tt>x</tt>. Choosing <tt>alpha := Bool</tt> will solve this, and in this case any solution will do; it's a bit like resolving an ambiguous type variable.
</p>
<p>
It's tricky in general, though. Suppose we had two constraints <tt>(X alpha ~ X Bool)</tt> and <tt>(Y alpha ~ Y Char)</tt>. Now we can't solve it so easily!
</p>
<p>
Worse, suppose we had an instance declaration
</p>
<pre class="wiki"> type instance Y Bool = Char
</pre><p>
Should we still resolve <tt>alpha := Bool</tt>? Would the answer change if there was a <em>second</em> instance?
</p>
<pre class="wiki"> type instance Y Int = Char
</pre><p>
Arguably, searching for all possible solutions is not terribly good.
</p>
<p>
It's not at all obvious what the Right Thing is.
</p>
<p>
Simon
</p>
TicketsimonpjMon, 23 Feb 2009 09:41:21 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:11
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:11
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3038" title="bug: Associated type use triggers a bogus error message (closed: duplicate)">#3038</a>
</p>
Ticketjim.stuttardSat, 21 Mar 2009 11:00:20 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:12
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:12
<p>
I don't know whether there's been a regression but with
</p>
<p>
Andres Loh's example i2 with:
</p>
<blockquote class="citation">
<p>
{-# TypeFamilies, EmptyDataDecls, RankNTypes #-}
</p>
</blockquote>
<blockquote class="citation">
<p>
type family Y (a::*)
</p>
</blockquote>
<blockquote class="citation">
<p>
i2 :: (forall a. a -> Y a) -> Y Bool
i2 x = x True
</p>
</blockquote>
<p>
I got:
</p>
<p>
"ghc panic! ..
</p>
<blockquote>
<p>
(GHC version 6.10.1 for i386-unknown-linux
TcTyFuns.flattenType: synonym family in a rank-n type"
</p>
</blockquote>
<p>
uname -a: Linux eeepc 2.26.28-ARCH
ghc -v: ghc-6.10.1 i386-unknown-linux
</p>
<p>
There's a lot to more to forall than meets the eye :)
Jim
</p>
Ticketjim.stuttardSat, 21 Mar 2009 11:04:30 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:13
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:13
<p>
with
</p>
<blockquote class="citation">
<p>
i2 x = x True
</p>
</blockquote>
Ticketjim.stuttardSat, 21 Mar 2009 18:10:12 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:14
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:14
<p>
what's wrong with this <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/WikiFormatting">WikiFormatting</a>?
1 blank line = zero blank lines.
</p>
TicketiglooSun, 12 Apr 2009 20:28:09 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:15
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:15
<ul>
<li><strong>milestone</strong>
changed from <em>6.10 branch</em> to <em>6.12 branch</em>
</li>
</ul>
TicketsimonpjTue, 14 Apr 2009 12:53:40 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:16
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:16
<p>
Yet another (killer) type-family example:
</p>
<pre class="wiki">class Key k where
type Map k :: * -> *
empty :: Map k v
instance Key a => Key (Maybe a) where
type Map (Maybe a) = MM a
empty = MM Nothing empty
data MM a v = MM (Maybe v) (Map a v)
</pre><p>
where we get
</p>
<pre class="wiki">Map.hs:27:21:
Couldn't match expected type `Map a' against inferred type `Map k'
In the second argument of `MM', namely `empty'
In the expression: MM Nothing empty
In the definition of `empty': empty = MM Nothing empty
</pre><p>
The terrible thing is that no amount of type signatures will fix this!
</p>
<p>
Simon
</p>
TicketsimonpjWed, 13 May 2009 09:31:27 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:17
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:17
<p>
See also <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3227" title="bug: Can't specify type signature of value typed with type families (closed: duplicate)">#3227</a>.
</p>
TicketiglooFri, 30 Apr 2010 16:39:20 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:18
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:18
<ul>
<li><strong>milestone</strong>
changed from <em>6.12 branch</em> to <em>6.12.3</em>
</li>
</ul>
TicketiglooSat, 19 Jun 2010 16:56:54 GMTpriority, milestone changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:19
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:19
<ul>
<li><strong>priority</strong>
changed from <em>normal</em> to <em>low</em>
</li>
<li><strong>milestone</strong>
changed from <em>6.12.3</em> to <em>6.14.1</em>
</li>
</ul>
TicketiglooSun, 19 Dec 2010 17:45:59 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:20
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:20
<ul>
<li><strong>milestone</strong>
changed from <em>7.0.1</em> to <em>7.0.2</em>
</li>
</ul>
TicketiglooSat, 05 Mar 2011 13:16:13 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:21
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:21
<ul>
<li><strong>milestone</strong>
changed from <em>7.0.2</em> to <em>7.2.1</em>
</li>
</ul>
TicketdsfSun, 03 Jul 2011 18:11:25 GMTblocking set
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:22
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:22
<ul>
<li><strong>blocking</strong>
set to <em>5296</em>
</li>
</ul>
TicketdsfSun, 03 Jul 2011 20:57:59 GMTcc changed; failure set
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:23
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:23
<ul>
<li><strong>cc</strong>
<em>dsf@…</em> added
</li>
<li><strong>failure</strong>
set to <em>None/Unknown</em>
</li>
</ul>
TicketliyangThu, 07 Jul 2011 02:43:16 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:24
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:24
<ul>
<li><strong>cc</strong>
<em>hackage.haskell.org@…</em> added
</li>
</ul>
Ticketsimonpj@…Tue, 16 Aug 2011 10:47:57 GMT
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:25
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:25
<p>
commit <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/49dbe60558deee5ea6cd2c7730b7c591d15559c8/ghc" title="Major improvement to pattern bindings
This patch makes a number of ...">49dbe60558deee5ea6cd2c7730b7c591d15559c8</a>
</p>
<pre class="wiki">Author: Simon Peyton Jones <simonpj@microsoft.com>
Date: Tue Aug 16 10:23:52 2011 +0100
Major improvement to pattern bindings
This patch makes a number of related improvements
a) Implements the Haskell Prime semantics for pattern bindings
(Trac #2357). That is, a pattern binding p = e is typed
just as if it had been written
t = e
f = case t of p -> f
g = case t of p -> g
... etc ...
where f,g are the variables bound by p. In paricular it's
ok to say
(f,g) = (\x -> x, \y -> True)
and f and g will get propertly inferred types
f :: a -> a
g :: a -> Int
b) Eliminates the MonoPatBinds flag altogether. (For the moment
it is deprecated and has no effect.) Pattern bindings are now
generalised as per (a). Fixes Trac #2187 and #4940, in the
way the users wanted!
c) Improves the OutsideIn algorithm generalisation decision.
Given a definition without a type signature (implying "infer
the type"), the published algorithm rule is this:
- generalise *top-level* functions, and
- do not generalise *nested* functions
The new rule is
- generalise a binding whose free variables have
Guaranteed Closed Types
- do not generalise other bindings
Generally, a top-level let-bound function has a Guaranteed
Closed Type, and so does a nested function whose free vaiables
are top-level functions, and so on. (However a top-level
function that is bitten by the Monomorphism Restriction does
not have a GCT.)
Example:
f x = let { foo y = y } in ...
Here 'foo' has no free variables, so it is generalised despite
being nested.
d) When inferring a type f :: ty for a definition f = e, check that
the compiler would accept f :: ty as a type signature for that
same definition. The type is rejected precisely when the type
is ambiguous.
Example:
class Wob a b where
to :: a -> b
from :: b -> a
foo x = [x, to (from x)]
GHC 7.0 would infer the ambiguous type
foo :: forall a b. Wob a b => b -> [b]
but that type would give an error whenever it is called; and
GHC 7.0 would reject that signature if given by the
programmer. The new type checker rejects it up front.
Similarly, with the advent of type families, ambiguous types are
easy to write by mistake. See Trac #1897 and linked tickets for
many examples. Eg
type family F a :: *
f ::: F a -> Int
f x = 3
This is rejected because (F a ~ F b) does not imply a~b. Previously
GHC would *infer* the above type for f, but was unable to check it.
Now even the inferred type is rejected -- correctly.
The main implemenation mechanism is to generalise the abe_wrap
field of ABExport (in HsBinds), from [TyVar] to HsWrapper. This
beautiful generalisation turned out to make everything work nicely
with minimal programming effort. All the work was fiddling around
the edges; the core change was easy!
compiler/deSugar/DsBinds.lhs | 62 +++-----
compiler/deSugar/DsExpr.lhs | 6 +-
compiler/hsSyn/HsBinds.lhs | 28 +++-
compiler/hsSyn/HsUtils.lhs | 32 +++--
compiler/main/DynFlags.hs | 13 +-
compiler/rename/RnBinds.lhs | 6 +-
compiler/typecheck/TcBinds.lhs | 282 ++++++++++++++++++++--------------
compiler/typecheck/TcClassDcl.lhs | 12 +-
compiler/typecheck/TcEnv.lhs | 117 +++++++++------
compiler/typecheck/TcErrors.lhs | 32 +++--
compiler/typecheck/TcHsSyn.lhs | 14 +-
compiler/typecheck/TcInstDcls.lhs | 19 ++-
compiler/typecheck/TcMType.lhs | 6 +-
compiler/typecheck/TcRnDriver.lhs | 14 +-
compiler/typecheck/TcRnMonad.lhs | 2 +-
compiler/typecheck/TcRnTypes.lhs | 11 +-
compiler/typecheck/TcSimplify.lhs | 57 +++++---
compiler/typecheck/TcTyClsDecls.lhs | 4 +-
compiler/typecheck/TcType.lhs | 28 ++--
19 files changed, 439 insertions(+), 306 deletions(-)
</pre>
TicketsimonpjTue, 16 Aug 2011 10:51:36 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:26
http://ghc.haskell.org/trac/ghc/ticket/1897#comment:26
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>testcase</strong>
set to <em>typecheck/should_compile/T1897a, indexed_types/should_compile/T1897b</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Done! See (d) in the commit message.
</p>
<p>
Simon
</p>
Ticket