Typechecker behaviour change

[igloo]

From:  http://www.haskell.org/pipermail/glasgow-haskell-users/2011-March/020116.html

The behaviour has changed (7.0.1 accepts it, 7.0.2 doesn't), but I'm not sure which behaviour is right.

I've put a cut-down (but not standalone) version of the offending module below. I believe the relevant steps are then:

The ct application means we need an instance for:
      Cast (ResidueI (Pol (ResidueE (UPol k))))
                     (Pol (ResidueE (UPol k)))

Need: Cast (ResidueI (Pol (ResidueE (UPol k))))
                     (Pol (ResidueE (UPol k)))
Have:     instance LinSolvRing a => Cast (ResidueI a) a

Now need: LinSolvRing (Pol (ResidueE (UPol k)))
Have:     instance EuclideanRing a => LinSolvRing (Pol a)

Now need: EuclideanRing (ResidueE (UPol k))
Have:     instance (EuclideanRing a, Ring (ResidueE a) )
                => EuclideanRing (ResidueE a)

Now need: EuclideanRing (UPol k)
Have:     instance Field a => EuclideanRing (UPol a)

Now need: LinSolvRing (UPol k)    (from the EuclideanRing class constraints)
Have:     instance EuclideanRing a => LinSolvRing (UPol a)  (Pol2_.hs:95)
And:      instance (LinSolvRing (Pol a), CommutativeRing a)
                => LinSolvRing (UPol (Pol a))

A different instance should be used depending on whether or not
    k = Pol x
(for some x).

With flags:

-XTypeSynonymInstances -XUndecidableInstances -XFlexibleContexts -XFlexibleInstances -XMultiParamTypeClasses -XOverlappingInstances -XRecordWildCards -XNamedFieldPuns -XScopedTypeVariables -fcontext-stack=30

module T_cubeext (cubicExt) where

import Prelude (undefined)
import DPrelude (ct)
import Categs (ResidueE)
import SetGroup ()
import RingModule (Field, FactorizationRing)
import VecMatr  ()
import Fraction ()
import Pol (Pol, UPol)
import Residue (ResidueI)
import GBasis  ()

cubicExt :: forall k . (Field k, FactorizationRing (UPol k))
         => k -> ()
cubicExt _ = undefined
 where unE :: ResidueI (Pol (ResidueE (UPol k)))
       unE  = undefined

       kToE :: Pol (ResidueE (UPol k)) -> ResidueI (Pol (ResidueE (UPol k)))
       kToE = ct unE

[simonpj]

GHC 7 indeed falls over on DoCon 2.12. It turns out to be a rather subtle interaction of overlapping instances with the ill-fated "silent superclass parameters" I introduced to solve a problem in the typechecker's constraint solver.

The problem is demonstrated in minature by test T5051, which I have added to the test suite, and I reproduce below for completeness.

Happily, silent parameters aren't needed any more (we solve the problem in another nicer way), so this patch removes them

commit a9d48fd94ae92b979610f5efe5d66506928118eb
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Wed Jun 22 11:46:03 2011 +0100

    Remove "silent superclass parameters"
    
    We introduced silent superclass parameters as a way to avoid
    superclass loops, but we now solve that problem a different
    way ("derived" superclass constraints carry no evidence). So
    they aren't needed any more.
    
    Apart from being a needless complication, they broke DoCon.
    Admittedly in a very obscure way, but still the result is
    hard to explain. To see the details see Trac #5051, with
    test case typecheck/should_compile/T5051.  (The test is
    nice and small!)

 compiler/basicTypes/Id.lhs                   |    7 +-
 compiler/basicTypes/IdInfo.lhs               |   12 +--
 compiler/basicTypes/MkId.lhs                 |   17 +--
 compiler/coreSyn/CoreSyn.lhs                 |    2 -
 compiler/coreSyn/CoreUnfold.lhs              |    1 -
 compiler/coreSyn/CoreUtils.lhs               |    2 +-
 compiler/coreSyn/PprCore.lhs                 |    1 -
 compiler/iface/BinIface.hs                   |    8 +-
 compiler/iface/IfaceSyn.lhs                  |    4 +-
 compiler/iface/MkIface.lhs                   |    2 +-
 compiler/iface/TcIface.lhs                   |    5 +-
 compiler/typecheck/TcErrors.lhs              |   12 +--
 compiler/typecheck/TcInstDcls.lhs            |  163 ++++++++++----------------
 compiler/typecheck/TcInteract.lhs            |   77 ++++--------
 compiler/typecheck/TcMType.lhs               |   22 +----
 compiler/types/InstEnv.lhs                   |   13 +--
 compiler/vectorise/Vectorise/Type/PADict.hs  |   73 +++++-------
 compiler/vectorise/Vectorise/Type/PRepr.hs   |   28 ++++-
 compiler/vectorise/Vectorise/Utils/PADict.hs |   16 +---
 19 files changed, 165 insertions(+), 300 deletions(-)

The fix will be be in GHC 7.2, but probably not in GHC 7.0. I've verified that 7.2 can compile DoCon? 2.12 and run the demotest.

Here's the tiny test

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

-- A very delicate interaction of overlapping instances

module T5051 where

data T = T deriving( Eq, Ord )
instance Eq [T] 

foo :: Ord a => [a] -> Bool
foo x = x >= x

-- Bizarrely, the defn of 'foo' failed in GHC 7.0.3 with
-- T5051.hs:14:10:
--    Overlapping instances for Eq [a]
--      arising from a use of `>'
--    Matching instances:
--      instance Eq a => Eq [a] -- Defined in GHC.Classes
--      instance [overlap ok] Eq [T] -- Defined at T5051.hs:9:10-15
--    (The choice depends on the instantiation of `a'
--     To pick the first instance above, use -XIncoherentInstances
--     when compiling the other instance declarations)
--    In the expression: x > x
--
-- Reason: the dfun for Ord [a] (in the Prelude) had a "silent"
-- superclass parameter, thus
--     $dfOrdList :: forall a. (Eq [a], Ord a) => Ord [a]
-- Using the dfun means we need Eq [a], and that gives rise to the
-- overlap error.
--
-- This is terribly confusing: the use of (>=) means we need Ord [a],
-- and if we have Ord a (which we do) we should be done.
-- A very good reason for not having silent parameters!

[simonpj]

I think we have to re-introduce silent superclass paramters (see #5751). And indeed, looking at the example above, arguably it should complain about overlap. Just suppose that the Ord instance for lists was declared like this:

instance Ord a => Ord [a] where
  x >= y == x>y || x==y

With this implementation, at type Ord [T] we really should be using the Eq [T] instance, so the overlap complaint for foo is absolutely right.

Serge: how bad would it be if we re-introduced the behaviour you reported in  http://www.haskell.org/pipermail/glasgow-haskell-users/2011-March/020116.html? I now think (a) it's the right behaviour (b) it's necessary to cure #5751.