default Int is ignored for argument of levity polymorphic method

See also: #25778 (closed)

Summary

test/Debug/TraceIf/Test/TraceIf/TH.hs:46:25: error: [GHC-43085]
    • Overlapping instances for Show t0 arising from a use of ‘show’
      Matching instance:
        instance P.Show a => Show a
          -- Defined at test/Debug/TraceIf/Test/TraceIf/TH.hs:35:10
      Potentially matching instance:
        instance Show (ShowTrace ())
          -- Defined at test/Debug/TraceIf/Test/TraceIf/TH.hs:38:10
      (The choice depends on the instantiation of ‘t0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the second argument of ‘(==)’, namely ‘show 1’
      In the expression: "1" == show 1
      In an equation for ‘unit_svarsWith’: unit_svarsWith = "1" == show 1
   |
46 | unit_svarsWith = "1" == show 1
   |                         ^^^^

test/Debug/TraceIf/Test/TraceIf/TH.hs:46:30: error: [GHC-39999]
    • Ambiguous type variable ‘t0’ arising from the literal ‘1’
      prevents the constraint ‘(Num t0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘t0’ should be.
      Potentially matching instances:
        instance Num Integer
          -- Defined in ‘ghc-internal-9.1001.0:GHC.Internal.Num’
        instance Num Double
          -- Defined in ‘ghc-internal-9.1001.0:GHC.Internal.Float’
        ...plus three others
        ...plus one instance involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the first argument of ‘show’, namely ‘1’
      In the second argument of ‘(==)’, namely ‘show 1’
      In the expression: "1" == show 1
   |
46 | unit_svarsWith = "1" == show 1

Steps to reproduce

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module Debug.TraceIf.Test.TraceIf.TH where

import GHC.Exts
import Prelude hiding (Show (..))
import Prelude qualified as P

default (Int)

class Show (t :: TYPE r) where
  show :: t -> String

newtype ShowTrace a = ShowTrace { unShowTrace :: a }

instance P.Show a => Show a where
  show = P.show

instance Show (ShowTrace ()) where
  show (ShowTrace ()) = "()"

unit_svarsWith :: Bool
unit_svarsWith = "1" == show 1

Expected behavior

Literal argument of show (1) should be typed as Int because of default (Int).

Show (ShowTrace ()) as a candidate looks wrong. ShowTrace () does not have Num instance.

Environment

• GHC version used: 9.10.1

Optional:

• Operating System: Linux
• System Architecture: x86_64

added needs triage label

#17201

This does look wrong.

Interestingly this works OK in HEAD. Maybe someone would care to bisect to see what fixed it?

@sheaf has been active in defaulting territory recently.

This is fixed in GHC 9.12, and I think it's very likely that it was fixed with the "exportable named defaults" patch !11853 (merged). I am investigating.

Here's a simpler reproducer with no levity polymorphism or anything of the sort. It seems that the default declaration is entirely ignored, which is very strange.

module T25775 where

default (Int)

class C t where
  meth :: t -> ()
instance C Int where
  meth _ = ()

one :: Num a => a
one = 1

ambig :: ()
ambig = meth one

It seems that the behaviour in the OP is as expected (as per the Haskell 98 report):

In situations where an ambiguous type is discovered, an ambiguous type variable, v, is defaultable if:

• v appears only in constraints of the form C v, where C is a class, and
• at least one of these classes is a numeric class, (that is, Num or a subclass of Num), and
• all of these classes are defined in the Prelude or a standard library

In the OP, the ambiguous type variable appears as an argument of a custom levity-polymorphic class (called Show, but it isn't Show from Prelude); in my previous example, it's the class C`.

So the implementation in GHC 9.10 and below is correct. However, the implementation of NamedDefaults changed this behaviour, as described in GHC Proposal #409

The new [defaulting] rules instead require only that:

• v appears in at least one constraint of the form C v, where C is a single-parameter class.

I believe the implementation doesn't follow this to the letter, as it still filters out type variables mentioned in non-unary constraints, but it deliberately omits the "all of the classes are standard class" part of the check.

What the proposal doesn't seem to be explicit about is whether this new defaulting behaviour should only happen when the NamedDefaults language extension is enabled. Because imports of default declarations happen whether one has enabled NamedDefaults or not, I think it makes sense to always use the new rules.

My conclusions:

1. The behaviour in GHC 9.10 and below is deliberate, and follows the Haskell Report.
2. The change in behaviour in GHC 9.12 is also deliberate.
3. The change in defaulting semantics should be documented more clearly in the user's guide as well as in the 9.12 changelog.
4. The implementation in GHC 9.12 and above needs to be adjusted to remove the requirement that a defaultable tyvar must not appear in any non-unary typeclasses.

mentioned in issue #25778 (closed)

added Pnormal Tquestion defaulting typechecker labels and removed needs triage label

added documentation label

assigned to @sheaf

I need to update the documentation on defaulting anyway, so I will try to include an explanation of the changes relating to this ticket as well.

changed the description

mentioned in merge request !14075 (closed)

mentioned in commit 0f9d2173

closed with commit f1acdd2c

mentioned in commit f1acdd2c