Kind-defaulting omitted leads to deeply obscure type error

Oleg writes:Here is the simpified code to reproduce the problem.

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverloadedStrings #-}

module P where

import GHC.Exts( IsString(..) )
import Data.Monoid

newtype DC d = DC d
    deriving (Show, Monoid)

instance IsString (DC String) where
    fromString = DC


class Monoid acc => Build acc r where
    type BuildR r :: *		-- Result type
    build :: (acc -> BuildR r) -> acc -> r

instance Monoid dc => Build dc (DC dx) where
    type BuildR (DC dx) = DC dx
    build tr acc = tr acc

instance (Build dc r, a ~ dc) => Build dc (a->r) where
    type BuildR (a->r) = BuildR r
    build tr acc s = build tr (acc `mappend` s)


-- The type is inferred
tspan :: (Monoid d, Build (DC d) r, BuildR r ~ DC d) => r
tspan = build (id :: DC d -> DC d) mempty

-- foo = tspan "aa"

-- foo1 = tspan (tspan "aa")

bar = tspan "aa" :: DC String

This compiles, but if I uncomment the definition foo, the compiler complains

/tmp/p.hs:39:1:
    Couldn't match type `[Char]' with `DC d'
    When checking that `foo'
      has the inferred type `forall t d a.
                             (IsString a, Monoid d, Build (DC d) (a -> t),
                              BuildR (a -> t) ~ DC d) =>
                             t'
    Probable cause: the inferred type is ambiguous

However, the same code on GHC 7.4.1 type checks with no problem. The compiler infers for foo:

foo :: (IsString (DC d), Monoid d, Build (DC d) t, BuildR t ~ DC d) => t

which is exactly as I would expect.

If you uncomment foo1, a much bigger error message emerges

/tmp/p.hs:41:1:
    Could not deduce (BuildR t0 ~ DC d0)
    from the context (IsString a,
                      Monoid d,
                      Monoid d1,
                      Build (DC d) (t1 -> t),
                      Build (DC d1) (a -> t1),
                      BuildR (a -> t1) ~ DC d1,
                      BuildR (t1 -> t) ~ DC d)
      bound by the inferred type for `foo1':
                 (IsString a, Monoid d, Monoid d1, Build (DC d) (t1 -> t),
                  Build (DC d1) (a -> t1), BuildR (a -> t1) ~ DC d1,
                  BuildR (t1 -> t) ~ DC d) =>
                 t
      at /tmp/p.hs:41:1-25
    The type variables `t0', `d0' are ambiguous
    Possible fix: add a type signature that fixes these type variable(s)
    Expected type: DC d0
      Actual type: BuildR (a0 -> t0)
    When checking that `foo1'
      has the inferred type `forall t d t1 d1 a.
                             (IsString a, Monoid d, Monoid d1, Build (DC d) (t1 -> t),
                              Build (DC d1) (a -> t1), BuildR (a -> t1) ~ DC d1,
                              BuildR (t1 -> t) ~ DC d) =>
                             t'
    Probable cause: the inferred type is ambiguous

The error message indeed sounds like there is a problem: the type variables t0 and d0 aren't mentioned anywhere else. However, GHC 7.4.1 does not have any problem with foo1. It accepts it and infers for it the same type as for foo. Again, this is what I'd expect.

Trac metadata

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