Inconsistent treatment of ambiguous instance signatures
This was originally spun out of #14266 (comment 142782), but this issue can be understood in isolation. Below are four programs:
-
{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE ScopedTypeVariables #-} class C a where m :: forall x. String instance C Bool where m :: forall x. String m = "Bool" -
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE ScopedTypeVariables #-} class C a where m :: forall x. String instance C Bool where m :: forall x. String m = "Bool" -
{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE ScopedTypeVariables #-} class C a where m :: forall x. Show x => String instance C Bool where m :: forall x. Show x => String m = "Bool" -
{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE ScopedTypeVariables #-} class C a where m :: forall x. Show x => String instance C Bool where m :: forall x. Show x => String m = "Bool"
Can you guess what GHC 8.8.3 will do when compiling ech of these programs?
-
This will be rejected:
$ /opt/ghc/8.8.3/bin/ghci Bug.hs GHCi, version 8.8.3: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:5:3: error: • Could not deduce (C a0) from the context: C a bound by the type signature for: m :: forall a x. C a => String at Bug.hs:5:3-23 The type variable ‘a0’ is ambiguous • In the ambiguity check for ‘m’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: m :: forall a x. C a => String In the class declaration for ‘C’ | 5 | m :: forall x. String | ^^^^^^^^^^^^^^^^^^^^^This makes sense, as the type of
mis genuinely ambiguous. The error message helpfully suggests enablingAllowAmbiguousTypes, and if we do so... -
...then we end up with program (2), which typechecks. Hooray!
-
As was the case with program (1), this program will be rejected:
$ /opt/ghc/8.8.3/bin/ghci Bug.hs GHCi, version 8.8.3: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:5:3: error: • Could not deduce (C a0) from the context: (C a, Show x) bound by the type signature for: m :: forall a x. (C a, Show x) => String at Bug.hs:5:3-33 The type variable ‘a0’ is ambiguous • In the ambiguity check for ‘m’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: m :: forall a x. (C a, Show x) => String In the class declaration for ‘C’ | 5 | m :: forall x. Show x => String | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^Again, this is sensible, since
m's type is also ambiguous. Experience has taught us that the solution is to enableAllowAmbiguousTypes, and if we do so... -
...then we end up with program (4). However, this still doesn't typecheck!
$ /opt/ghc/8.8.3/bin/ghci Bug.hs GHCi, version 8.8.3: https://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:8:8: error: • Could not deduce (Show x0) from the context: Show x bound by the type signature for: m :: forall x. Show x => String at Bug.hs:8:8-33 The type variable ‘x0’ is ambiguous • When checking that instance signature for ‘m’ is more general than its signature in the class Instance sig: forall x. Show x => String Class sig: forall x. Show x => String In the instance declaration for ‘C Bool’ | 8 | m :: forall x. Show x => String | ^^^^^^^^^^^^^^^^^^^^^^^^^^How bizarre. Why did the trick of enabling
AllowAmbiguousTypeswork for program (2), but not for program (4)?
At first, I thought that perhaps there was something special about constraint arguments like Show x =>. But I don't think that this is the case, since if you remove the C Bool instance from program (4):
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ScopedTypeVariables #-}
class C a where
m :: forall x. Show x => StringThen it typechecks without issue. This leads me to believe that there is some inconsistency in the way that instance signatures are checked for ambiguity, especially when compared to the way other type signatures are checked for ambiguity. Some digging into the source code appears to support my hypothesis. Here is the code that checks instance signatures for ambiguity (in TcInstDecls.tcMethodBodyHelp):
; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $
tcSubType_NC ctxt sig_ty local_meth_tyAnd here is the code that checks other signatures for ambiguity (in TcValidity.checkAmbiguity):
; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $
captureConstraints $
tcSubType_NC ctxt ty ty
; simplifyAmbiguityCheck ty wantedNotice how the latter code uses simplifyAmbiguityCheck, but the former does not. I believe that this is a crucial distinction, because simplifyAmbiguityCheck has special logic for discarding errors depending on whether or not AllowAmbiguousTypes is enabled:
simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
simplifyAmbiguityCheck ty wanteds
= do { ...
-- Normally report all errors; but with -XAllowAmbiguousTypes
-- report only insoluble ones, since they represent genuinely
-- inaccessible code
; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
; traceTc "reportUnsolved(ambig) {" empty
; unless (allow_ambiguous && not (insolubleWC final_wc))
(discardResult (reportUnsolved final_wc))
; ... }This might explain why forall x. Show x => String is ambiguous only as an instance signature.