Opened 8 years ago
Closed 5 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 simonpj)
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 8 years ago by guest
comment:1 Changed 8 years ago by igloo
- Component changed from Compiler to Compiler (Type checker)
- difficulty set to Unknown
- Milestone set to 6.10 branch
- Owner set to chak
comment:2 Changed 8 years ago by pgavin
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 8 years ago by chak
- Resolution set to invalid
- Status changed from new to closed
This is not a bug, see the discussion in the mailing list URL of the previous comment.
comment:4 Changed 8 years ago by simonpj
- Priority changed from normal to low
- Resolution invalid deleted
- Status changed from closed to 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 8 years ago by Isaac Dupree
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 7 years ago by simonpj
- Priority changed from low to normal
See also #2157 and #2569. And Ganesh's email http://www.mail-archive.com/[email protected]/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:7 Changed 7 years ago by simonpj
See also #2855 (another instance of the same problem).
comment:8 Changed 7 years ago by simonpj
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 7 years ago by simonpj
- Description modified (diff)
- Summary changed from Type families: type signature rejected to Ambiguous types and rejected type signatures
comment:10 Changed 7 years ago by simonpj
- 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:11 Changed 7 years ago by simonpj
See also #3038
comment:12 Changed 7 years ago by jim.stuttard
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:13 Changed 7 years ago by jim.stuttard
with
i2 x = x True
comment:14 Changed 7 years ago by jim.stuttard
what's wrong with this WikiFormatting? 1 blank line = zero blank lines.
comment:15 Changed 7 years ago by igloo
- Milestone changed from 6.10 branch to 6.12 branch
comment:16 Changed 7 years ago by simonpj
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:17 Changed 7 years ago by simonpj
See also #3227.
comment:18 Changed 6 years ago by igloo
- Milestone changed from 6.12 branch to 6.12.3
comment:19 Changed 6 years ago by igloo
- Milestone changed from 6.12.3 to 6.14.1
- Priority changed from normal to low
comment:20 Changed 5 years ago by igloo
- Milestone changed from 7.0.1 to 7.0.2
comment:21 Changed 5 years ago by igloo
- Milestone changed from 7.0.2 to 7.2.1
comment:22 Changed 5 years ago by dsf
- Blocking 5296 added
comment:23 Changed 5 years ago by dsf
- Cc dsf@… added
- Type of failure set to None/Unknown
comment:24 Changed 5 years ago by liyang
- Cc hackage.haskell.org@… added
comment:25 Changed 5 years ago by simonpj@…
commit 49dbe60558deee5ea6cd2c7730b7c591d15559c8
Author: Simon Peyton Jones <[email protected]> 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 5 years ago by simonpj
- Resolution set to fixed
- Status changed from new to closed
- Test Case set to 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.