#7279: warning for unused type variables in instance contexts;
-fwarn-unreachable-
type-variables?
------------------------------------------+---------------------------------
Reporter: nfrisby | Owner:
Type: feature request | Status: closed
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.6.1
Resolution: fixed | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Difficulty: Unknown
Testcase: typecheck/should_fail/T7279 | Blockedby:
Blocking: | Related:
------------------------------------------+---------------------------------
Changes (by simonpj):
* status: new => closed
* difficulty: => Unknown
* resolution: => fixed
* testcase: => typecheck/should_fail/T7279
Comment:
This fix to ambiguity checking solves the problem
{{{
commit 97db0edc4e637dd61ec635d1f9b6b6dd25ad890c
Author: Simon Peyton Jones <simo...@microsoft.com>
Date: Tue Jan 8 08:26:40 2013 +0000
Re-engineer the ambiguity test for user type signatures
Two main changes. First, re-engineer the ambiguity test. Previously
TcMType.checkAmbiguity used a rather syntactic test to detect some
types that are certainly ambiguous. But a much easier test is
available,
and it is used for inferred types in TcBinds. Namely
<type> is ambiguous
iff
<type> `TcUnify.isSubType` <type>
fails to hold, where "isSubType" means "is provably more polymorphic
than".
Example:
C a => Int
is ambiguous, because isSubType instantiates the (C a => Int)
to (C alpha => Int) and then tries to deduce (C alpha) from (C a).
This is
Martin Sulzmann's definition of ambiguity. (Defn 10 of "Understanding
functional dependencies via constraint handling rules", JFP.)
This change is neat, reduces code, and correctly rejects more
programs.
However is *is* just possible to have a useful program that would be
rejected. For example
class C a b
f :: C Int b => Int -> Int
Here 'f' would be rejected as having an ambiguous type. But it is
just possible that, at a *call* site there might be an instance
declaration instance C Int b, which does not constrain 'b' at all.
This is pretty strange -- why is 'b' overloaded at all? -- but it's
possible, so I also added a flag -XAllowAmbiguousTypes that simply
removes the ambiguity check. Let's see if anyone cares. Meanwhile
the earlier error report will be useful for everyone else.
A handful of regression tests had to be adjusted as a result, because
they used ambiguous types, somewhat accidentally.
Second, split TcMType (already too large) into two
* TcMType: a low-level module dealing with monadic operations like
zonking, creating new evidence variables, etc
* TcValidity: a brand-new higher-level module dealing with
validity checking for types: checkValidType, checkValidInstance,
checkFamInstPats etc
Apart from the fact that TcMType was too big, this allows TcValidity
to import TcUnify(tcSubType) without causing a loop.
compiler/ghc.cabal.in | 1 +
compiler/main/DynFlags.hs | 2 +
compiler/typecheck/TcBinds.lhs | 28 +-
compiler/typecheck/TcDeriv.lhs | 132 +++++
compiler/typecheck/TcErrors.lhs | 143 ++---
compiler/typecheck/TcEvidence.lhs | 4 +-
compiler/typecheck/TcHsType.lhs | 1 +
compiler/typecheck/TcInstDcls.lhs | 1 +
compiler/typecheck/TcMType.lhs | 1063
+----------------------------------
compiler/typecheck/TcPat.lhs | 1 +
compiler/typecheck/TcRnTypes.lhs | 8 +-
compiler/typecheck/TcSMonad.lhs | 9 +-
compiler/typecheck/TcSimplify.lhs | 152 +-----
compiler/typecheck/TcTyClsDecls.lhs | 1 +
14 files changed, 248 insertions(+), 1298 deletions(-)
}}}
Now the instance declaration will (rightly) be rejected as ambiguous. So
either you get
{{{
T7279.hs:5:10:
Variable `b' occurs more often than in the instance head
in the constraint: Show b
(Use -XUndecidableInstances to permit this)
In the instance declaration for `Eq (T a)'
}}}
or, if you add `-XUndecidableInstances` you get the ambiguity error
instead:
{{{
T7279.hs:6:10:
Could not deduce (Show b0)
arising from the ambiguity check for an instance declaration
from the context (Eq a, Show b)
bound by an instance declaration: (Eq a, Show b) => Eq (T a)
at T7279.hs:6:10-35
The type variable `b0' is ambiguous
In the ambiguity check for: forall a b. (Eq a, Show b) => Eq (T a)
In the instance declaration for `Eq (T a)'
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7279#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
