#5595: Unification under a forall doesn't allow full constraint solving
---------------------------------+------------------------------------------
Reporter: basvandijk | Owner: simonpj
Type: bug | Status: new
Priority: normal | Milestone: 7.6.1
Component: Compiler | Version: 7.2.1
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: GHC rejects valid program
---------------------------------+------------------------------------------
Comment(by simonpj@…):
commit 2e6dcdf711ebd50eef230a878014a5a9abd20e07
{{{
Author: Simon Peyton Jones <[email protected]>
Date: Mon Dec 5 04:44:13 2011 +0000
Allow full constraint solving under a for-all (Trac #5595)
The main idea is that when we unify
forall a. t1 ~ forall a. t2
we get constraints from unifying t1~t2 that mention a.
We are producing a coercion witnessing the equivalence of
the for-alls, and inside *that* coercion we need bindings
for the solved constraints arising from t1~t2.
We didn't have way to do this before. The big change is
that here's a new type TcEvidence.TcCoercion, which is
much like Coercion.Coercion except that there's a slot
for TcEvBinds in it.
This has a wave of follow-on changes. Not deep but broad.
* New module TcEvidence, which now contains the HsWrapper
TcEvBinds, EvTerm etc types that used to be in HsBinds
* The typechecker works exclusively in terms of TcCoercion.
* The desugarer converts TcCoercion to Coercion
* The main payload is in TcUnify.unifySigmaTy. This is the
function that had a gross hack before, but is now beautiful.
* LCoercion is gone! Hooray.
Many many fiddly changes in conssequence. But it's nice.
compiler/deSugar/Desugar.lhs | 2 +-
compiler/deSugar/DsArrows.lhs | 1 +
compiler/deSugar/DsBinds.lhs | 273 ++++++++--------
compiler/deSugar/DsExpr.lhs | 37 +--
compiler/deSugar/DsListComp.lhs | 1 +
compiler/deSugar/Match.lhs | 20 +-
compiler/deSugar/MatchCon.lhs | 13 +-
compiler/ghc.cabal.in | 1 +
compiler/hsSyn/HsBinds.lhs | 227 +-------------
compiler/hsSyn/HsExpr.lhs | 1 +
compiler/hsSyn/HsPat.lhs | 1 +
compiler/hsSyn/HsUtils.lhs | 66 ++--
compiler/main/GHC.hs | 2 +-
compiler/main/GhcMake.hs | 2 +-
compiler/parser/Parser.y.pp | 1 +
compiler/parser/RdrHsSyn.lhs | 1 +
compiler/rename/RnBinds.lhs | 1 +
compiler/typecheck/Inst.lhs | 3 +-
compiler/typecheck/TcArrows.lhs | 6 +-
compiler/typecheck/TcBinds.lhs | 1 +
compiler/typecheck/TcCanonical.lhs | 123 ++++----
compiler/typecheck/TcClassDcl.lhs | 1 +
compiler/typecheck/TcDeriv.lhs | 12 +-
compiler/typecheck/TcEnv.lhs | 8 +-
compiler/typecheck/TcEvidence.lhs | 570
+++++++++++++++++++++++++++++++++
compiler/typecheck/TcExpr.lhs | 12 +-
compiler/typecheck/TcForeign.lhs | 2 +-
compiler/typecheck/TcHsSyn.lhs | 53 ++--
compiler/typecheck/TcHsType.lhs | 1 +
compiler/typecheck/TcInstDcls.lhs | 14 +-
compiler/typecheck/TcInteract.lhs | 55 ++--
compiler/typecheck/TcMatches.lhs | 6 +-
compiler/typecheck/TcMatches.lhs-boot | 3 +-
compiler/typecheck/TcPat.lhs | 22 +-
compiler/typecheck/TcRnDriver.lhs | 3 +-
compiler/typecheck/TcRnMonad.lhs | 7 +-
compiler/typecheck/TcRnTypes.lhs | 5 +
compiler/typecheck/TcSMonad.lhs | 82 ++---
compiler/typecheck/TcSimplify.lhs | 5 +-
compiler/typecheck/TcSplice.lhs | 1 +
compiler/typecheck/TcType.lhs | 10 +-
compiler/typecheck/TcUnify.lhs | 79 ++---
compiler/typecheck/TcUnify.lhs-boot | 4 +-
compiler/types/Coercion.lhs | 98 ++-----
compiler/types/Type.lhs | 9 +-
compiler/types/TypeRep.lhs | 2 +-
46 files changed, 1079 insertions(+), 768 deletions(-)
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5595#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
