Ambiguous types and rejected type signatures

[guest]

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@…)

[igloo]

Thanks for the report. Looks like one for you, Manuel.

[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

[chak]

This is not a bug, see the discussion in the mailing list URL of the previous comment.

[simonpj]

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

[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.

[simonpj]

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

[simonpj]

See also #2855 (another instance of the same problem).

[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

[simonpj]

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

[simonpj]

See also #3038

[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

[jim.stuttard]

with

i2 x = x True

[jim.stuttard]

what's wrong with this WikiFormatting? 1 blank line = zero blank lines.

[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

[simonpj]

See also #3227.

[simonpj@…]

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(-)

[simonpj]

Done! See (d) in the commit message.

Simon