[GHC] #7332: Kind-defaulting omitted leads to deeply obscure type error

[GHC]

#7332: Kind-defaulting omitted leads to deeply obscure type error
---------------------------------+------------------------------------------
    Reporter:  simonpj           |       Owner:                  
        Type:  bug               |      Status:  new             
    Priority:  normal            |   Milestone:                  
   Component:  Compiler          |     Version:  7.6.1           
    Keywords:                    |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |     Failure:  None/Unknown    
  Difficulty:  Unknown           |    Testcase:                  
   Blockedby:                    |    Blocking:                  
     Related:                    |  
---------------------------------+------------------------------------------
 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.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7332>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler