Ambiguous types with constraints on new variables

The following code fails to compile:

{-# LANGUAGE FlexibleContexts, TypeFamilies #-}

import Data.Typeable

type family Foo a

data C a

foo :: (Typeable (C z), z ~ Foo zp) => C zp
foo = undefined

with the error

    • Could not deduce (Typeable z)
      from the context: (Typeable (C z), z ~ Foo zp)
        bound by the type signature for:
                   foo :: (Typeable (C z), z ~ Foo zp) => C zp
        at Bug.hs:(9,8)-(10,9)
    • In the ambiguity check for ‘foo’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        foo :: (Typeable (C z), z ~ Foo zp) => C zp

It's quite unclear why GHC feels thta it needs Typeable z. The code compiles if I change the Typeable constraint to Typeable (C (Foo zp)), which should be identical to what I wrote.

Trac metadata

Trac field	Value
Version	8.0.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

You are walking on thin ice. Consider

f :: Eq [a] => [a] -> [a]
f x = [x] == [x]

From the RHS we need Eq [a] which is provided by the type signature. But GHC could also solve Eq [a] by using instance Eq a => Eq [a] (which is usually the right thing to do). Then it would need Eq a, which it cannot get from Eq a. To avoid this dead end GHC tries to solve "wanted" constraints from "givens" first.

But what if it was

f :: (Eq b, b ~ [a]) => [a] -> [a]
f x = [x] == [x]

Now it's not quite so obvious. I would have expected this still to work, just, because equalities are always solved first. But the ice is a bit thinner.

I would have expected your example to work too, just. And so it does in HEAD, and hence in 8.2. But it'd be much more robust to put (Typeable z) in the context. Is there some reason you can't do that?

I'll add your example as a regression test and close as 'worksforme'.

Simon

mentioned in commit eb6ccb7c

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedWorksForMe

Simon, your explanation seems similar to #11948 (closed). Are they related?

I'm still wondering about this ticket. Why am I getting an ambiguous type error, and since the definition is undefined, why does GHC have to do any work at all?

Why am I getting an ambiguous type error

The "ambiguous type" check works like this. Suppose we have

foo :: ty
foo = blah

When is foo's type ambiguous? Answer: consider

foo2 :: ty
foo2 = foo

Does foo2 typecheck OK? If not, foo's type is ambiguous. Classic example

foo :: (Read a, Show a) =>  String -> String
foo x = show (read x)

foo2 :: (Read a, Show a) =>  String -> String
foo2 = foo  -- Error!

Now in your case we try

foo2 :: (Typeable (C z), z ~ Foo zp) => C zp
foo2 = foo

and it's this check (i.e. precisely the ambiguous-type test) that fails.

added Pnormal label