Opened 10 years ago
Closed 6 years ago
#1897 closed bug (fixed)
Ambiguous types and rejected type signatures
Reported by: | guest | Owned by: | chak |
---|---|---|---|
Priority: | low | Milestone: | 7.2.1 |
Component: | Compiler (Type checker) | Version: | 6.9 |
Keywords: | Cc: | andres@…, dsf@…, hackage.haskell.org@… | |
Operating System: | Linux | Architecture: | x86 |
Type of failure: | None/Unknown | Test Case: | typecheck/should_compile/T1897a, indexed_types/should_compile/T1897b |
Blocked By: | Blocking: | #5296 | |
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description (last modified by )
This ticket collects a bunch of examples where GHC
- 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.
- Accepts type signatures that are utterly ambiguous; that is, the function could never be called, or only in the presence of bizarre instance declarations.
- Rejects definitions that clearly have a unique typing.
Original example: the following programm does not compile:
{-# 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
Error:
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.
When one elides the type signature the program compiles yielding the offending signature:
Prelude> :r [1 of 1] Compiling Main ( GHC-Bug.hs, interpreted ) Ok, modules loaded: Main. *Main> :t isValid isValid :: (Bug a) => [Depend a] -> Bool
Compiler version: 6.9.20071105
Best regards,
Harald Holtmann (haskell@…)
Attachments (1)
Change History (27)
Changed 10 years ago by
Attachment: | GHC-Bug.hs added |
---|
comment:1 Changed 10 years ago by
Component: | Compiler → Compiler (Type checker) |
---|---|
difficulty: | → Unknown |
Milestone: | → 6.10 branch |
Owner: | set to chak |
comment:2 Changed 10 years ago by
just a note: it seems that the following thread may apply, in case someone else runs into this problem:
http://www.haskell.org/pipermail/haskell-cafe/2008-April/041397.html
comment:3 Changed 10 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
This is not a bug, see the discussion in the mailing list URL of the previous comment.
comment:4 Changed 10 years ago by
Priority: | normal → low |
---|---|
Resolution: | invalid |
Status: | closed → reopened |
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.
Simon
comment:5 Changed 10 years ago by
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.
foo :: (Show a, Read a) => Int foo = 1 where x = show (read "xxx")
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
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?
How about
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
Admittedly "reachable" might confuse people who don't think about what it means. It can be affected by equality constraints, for example. (is foo :: (a ~ Char, Show a, Read a) => Int; foo = 1
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 foo :: (a ~ Int) => F a -> F a; foo = id
is perfectly fine) (Also, in this case, leaving foldM next start ds
without a type-signature inside the type-information-losing isJust
, ensures that isJust (foldM next start ds)
has no usable type, for any ds
.)
If we reject the explicit type signature of foo :: F a -> F a; foo = id
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?:
foo = 1 where x = show (read "xxx")
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)
But I might have been wrong: isJust (foldM next start ds)
is just as bad as show . read
: 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.
comment:6 Changed 9 years ago by
Priority: | low → normal |
---|
See also #2157 and #2569. And Ganesh's email http://www.mail-archive.com/haskell-cafe@haskell.org/msg39593.html
We're now convinced that
- There is really no good way to check the type of functions like
isValid
- 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.
Simon
comment:8 Changed 9 years ago by
See also http://haskell.org/haskellwiki/GHC/Type_system#Type_signatures_and_ambiguity for an example unrelated to type functions.
See also #2885 for yet another example.
We must sort out this ambiguity problem.
Simon
comment:9 Changed 9 years ago by
Description: | modified (diff) |
---|---|
Summary: | Type families: type signature rejected → Ambiguous types and rejected type signatures |
comment:10 Changed 9 years ago by
Cc: | andres@… added |
---|
Here is yet another example, this time from Andres Loeh:
{-# 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
The definition i3
is currently rejected, because we can't determine that Y alpha ~ Y Bool
, where alpha
is an otherwise unconstrained unification variable, that comes from instantiating the occurrence of x
. Choosing alpha := Bool
will solve this, and in this case any solution will do; it's a bit like resolving an ambiguous type variable.
It's tricky in general, though. Suppose we had two constraints (X alpha ~ X Bool)
and (Y alpha ~ Y Char)
. Now we can't solve it so easily!
Worse, suppose we had an instance declaration
type instance Y Bool = Char
Should we still resolve alpha := Bool
? Would the answer change if there was a second instance?
type instance Y Int = Char
Arguably, searching for all possible solutions is not terribly good.
It's not at all obvious what the Right Thing is.
Simon
comment:12 Changed 9 years ago by
I don't know whether there's been a regression but with
Andres Loh's example i2 with:
{-# TypeFamilies, EmptyDataDecls, RankNTypes #-}
type family Y (a::*)
i2 :: (forall a. a -> Y a) -> Y Bool i2 x = x True
I got:
"ghc panic! ..
(GHC version 6.10.1 for i386-unknown-linux TcTyFuns.flattenType: synonym family in a rank-n type"
uname -a: Linux eeepc 2.26.28-ARCH ghc -v: ghc-6.10.1 i386-unknown-linux
There's a lot to more to forall than meets the eye :) Jim
comment:14 Changed 9 years ago by
what's wrong with this WikiFormatting? 1 blank line = zero blank lines.
comment:15 Changed 9 years ago by
Milestone: | 6.10 branch → 6.12 branch |
---|
comment:16 Changed 9 years ago by
Yet another (killer) type-family example:
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)
where we get
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
The terrible thing is that no amount of type signatures will fix this!
Simon
comment:18 Changed 8 years ago by
Milestone: | 6.12 branch → 6.12.3 |
---|
comment:19 Changed 8 years ago by
Milestone: | 6.12.3 → 6.14.1 |
---|---|
Priority: | normal → low |
comment:20 Changed 7 years ago by
Milestone: | 7.0.1 → 7.0.2 |
---|
comment:21 Changed 7 years ago by
Milestone: | 7.0.2 → 7.2.1 |
---|
comment:22 Changed 6 years ago by
Blocking: | 5296 added |
---|
comment:23 Changed 6 years ago by
Cc: | dsf@… added |
---|---|
Type of failure: | → None/Unknown |
comment:24 Changed 6 years ago by
Cc: | hackage.haskell.org@… added |
---|
comment:25 Changed 6 years ago by
commit 49dbe60558deee5ea6cd2c7730b7c591d15559c8
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(-)
comment:26 Changed 6 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Test Case: | → typecheck/should_compile/T1897a, indexed_types/should_compile/T1897b |
Done! See (d) in the commit message.
Simon
Thanks for the report. Looks like one for you, Manuel.