Opened 3 years ago

Closed 2 years ago

#7332 closed bug (fixed)

Kind-defaulting omitted leads to deeply obscure type error

Reported by: simonpj Owned by:
Priority: high Milestone: 7.8.1
Component: Compiler Version: 7.6.1
Keywords: Cc: oleg@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T7332
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

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.

Change History (10)

comment:1 Changed 3 years ago by simonpj

  • Milestone set to 7.8.1
  • Priority changed from normal to high

Good catch! In the transition from 7.4 I simplified the way that let-generalised types are inferred, and in so doing introduced an error. In this case it's because we infer a constraint Build (DC d) (a -> t), where a :: OpenKind.... and that means it doesn't match the instance declaration. However it is defaulted to a : * during quantification, and the result is very confusing and wrong.

Happily it's easy to fix. Patch coming.

Simon

comment:2 Changed 3 years ago by simonpj

  • Cc oleg@… added

comment:3 Changed 3 years ago by simonpj@…

commit 743582514c068c34235af2750dd5a726e981b77c

Author: Simon Peyton Jones <[email protected]>
Date:   Mon Oct 15 10:56:22 2012 +0100

    Add kind-defaulting in simplifyInfer (fixes Trac #7332)
    
    The basic point here is described in TcSimplify
       Note [Promote _and_ default when inferring]
    The new thing is that, when figuring out the predicates
    to abstact over in simplifyInfer, we must default OpenKind
    to *, just as we do in quantifyTyVar. I had not realised
    how important this was until Oleg came up with Trac #7332.
    
    As usual I did some refactoring, so the patch affects
    many more lines than strictly necessary.

 compiler/typecheck/TcSimplify.lhs |  266 ++++++++++++++++++-------------------
 1 files changed, 129 insertions(+), 137 deletions(-)

comment:4 Changed 3 years ago by simonpj

  • Status changed from new to merge
  • Test Case set to polykinds/T7332

comment:5 Changed 2 years ago by igloo

  • Status changed from merge to new

comment:6 Changed 2 years ago by igloo

  • Milestone changed from 7.8.1 to 7.6.2
  • Owner set to simonpj

Simon, could you take a look at fixing this on the 7.6 branch please? (or close it if you don't think it's worth the effort).

comment:7 Changed 2 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed

I think it's Too Bad for 7.6, I'm afraid.

comment:8 Changed 2 years ago by simonpj

Trac #7641 is a simpler example

comment:9 Changed 2 years ago by guest

  • Owner simonpj deleted
  • Resolution fixed deleted
  • Status changed from closed to new

I am sorry to bringing this problem back, but has it really been fixed? I have just upgraded
GHC to 7.6.3 and see exactly the same problem as reported in the original ticket. I use exactly the same file and receive the same problematic error messages. Perhaps some extra compiler flag is needed?

comment:10 Changed 2 years ago by igloo

  • Milestone changed from 7.6.2 to 7.8.1
  • Resolution set to fixed
  • Status changed from new to closed

It's fixed in the 7.8 branch, but not 7.6.

Note: See TracTickets for help on using tickets.