[commit: ghc] master: Fix an outright bug in the unflattener (b1ea047)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/b1ea0475894713b9fc753bf288589e0dc3175083/ghc

>---------------------------------------------------------------

commit b1ea0475894713b9fc753bf288589e0dc3175083
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Dec 14 13:25:48 2017 +0000

    Fix an outright bug in the unflattener
    
    Trac #14554 showed up an outright bug in the unflattening code in
    TcFlatten.  I was filling in a coercion with the wrong coercion (a Syn
    in the wrong place).  Result: "Bad coercion hole" assertion failures,
    and Core Lint Errors.
    
    Easily fixed, and the code is simpler too.


>---------------------------------------------------------------

b1ea0475894713b9fc753bf288589e0dc3175083
 compiler/typecheck/TcFlatten.hs                    | 45 ++++++++++++----------
 .../tests/indexed-types/should_compile/T14554.hs   | 34 ++++++++++++++++
 testsuite/tests/indexed-types/should_compile/all.T |  1 +
 3 files changed, 59 insertions(+), 21 deletions(-)

diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index c8479a6..ff4195c 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1571,11 +1571,13 @@ unflattenWanteds tv_eqs funeqs
         do { is_filled <- isFilledMetaTyVar tv
            ; elim <- case is_filled of
                False -> do { traceTcS "unflatten_eq 2" (ppr ct)
-                           ; tryFill      ev eq_rel       tv rhs }
-               True  -> do { traceTcS "unflatten_eq 2" (ppr ct)
-                           ; try_fill_rhs ev eq_rel tclvl tv rhs }
-           ; if elim then return rest
-                     else return (ct `consCts` rest) }
+                           ; tryFill ev tv rhs }
+               True  -> do { traceTcS "unflatten_eq 3" (ppr ct)
+                           ; try_fill_rhs ev tclvl tv rhs }
+           ; if elim
+             then do { setReflEvidence ev eq_rel (mkTyVarTy tv)
+                     ; return rest }
+             else return (ct `consCts` rest) }
 
       | otherwise
       = return (ct `consCts` rest)
@@ -1583,7 +1585,7 @@ unflattenWanteds tv_eqs funeqs
     unflatten_eq _ ct _ = pprPanic "unflatten_irred" (ppr ct)
 
     ----------------
-    try_fill_rhs ev eq_rel tclvl lhs_tv rhs
+    try_fill_rhs ev tclvl lhs_tv rhs
          -- Constraint is lhs_tv ~ rhs_tv,
          -- and lhs_tv is filled, so try RHS
       | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
@@ -1595,7 +1597,7 @@ unflattenWanteds tv_eqs funeqs
                               -- not unify with
       = do { is_filled <- isFilledMetaTyVar rhs_tv
            ; if is_filled then return False
-             else tryFill ev eq_rel rhs_tv
+             else tryFill ev rhs_tv
                           (mkTyVarTy lhs_tv `mkCastTy` mkSymCo co) }
 
       | otherwise
@@ -1618,26 +1620,27 @@ unflattenWanteds tv_eqs funeqs
 
     finalise_eq ct _ = pprPanic "finalise_irred" (ppr ct)
 
-tryFill :: CtEvidence -> EqRel -> TcTyVar -> TcType -> TcS Bool
+tryFill :: CtEvidence -> TcTyVar -> TcType -> TcS Bool
 -- (tryFill tv rhs ev) assumes 'tv' is an /un-filled/ MetaTv
 -- If tv does not appear in 'rhs', it set tv := rhs,
 -- binds the evidence (which should be a CtWanted) to Refl<rhs>
 -- and return True.  Otherwise returns False
-tryFill ev eq_rel tv rhs
+tryFill ev tv rhs
   = ASSERT2( not (isGiven ev), ppr ev )
     do { rhs' <- zonkTcType rhs
-       ; case tcGetTyVar_maybe rhs' of {
-            Just tv' | tv == tv' -> do { setReflEvidence ev eq_rel rhs
-                                       ; return True } ;
-            _other ->
-    do { case occCheckExpand tv rhs' of
-           Just rhs''    -- Normal case: fill the tyvar
-             -> do { setReflEvidence ev eq_rel rhs''
-                   ; unifyTyVar tv rhs''
-                   ; return True }
-
-           Nothing ->  -- Occurs check
-                      return False } } }
+       ; case () of
+            _ | Just tv' <- tcGetTyVar_maybe rhs'
+              , tv == tv'   -- tv == rhs
+              -> return True
+
+            _ | Just rhs'' <- occCheckExpand tv rhs'
+              -> do {       -- Fill the tyvar
+                      unifyTyVar tv rhs''
+                    ; return True }
+
+            _ | otherwise   -- Occurs check
+              -> return False
+    }
 
 setReflEvidence :: CtEvidence -> EqRel -> TcType -> TcS ()
 setReflEvidence ev eq_rel rhs
diff --git a/testsuite/tests/indexed-types/should_compile/T14554.hs b/testsuite/tests/indexed-types/should_compile/T14554.hs
new file mode 100644
index 0000000..f6b3822
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T14554.hs
@@ -0,0 +1,34 @@
+{-# Language UndecidableInstances, DataKinds, TypeOperators,
+             KindSignatures, PolyKinds, TypeInType, TypeFamilies,
+             GADTs, LambdaCase, ScopedTypeVariables #-}
+
+module T14554 where
+
+import Data.Kind
+import Data.Proxy
+
+type a ~> b = (a, b) -> Type
+
+data IdSym0 :: (Type,Type) -> Type
+
+data KIND = X | FNARR KIND KIND
+
+data TY :: KIND -> Type where
+  ID    :: TY (FNARR X X)
+  FNAPP :: TY (FNARR k k') -> TY k -> TY k'
+
+data TyRep (kind::KIND) :: TY kind -> Type where
+  TID    :: TyRep (FNARR X X)  ID
+  TFnApp :: TyRep (FNARR k k') f
+         -> TyRep k            a
+         -> TyRep k'           (FNAPP f a)
+
+type family IK (kind::KIND) :: Type where
+  IK X            = Type
+  IK (FNARR k k') = IK k ~> IK k'
+
+type family IT (ty::TY kind) :: IK kind
+
+zero :: TyRep X a -> IT a
+zero x = case x of
+            TFnApp TID a -> undefined
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 6407324..9250fa2 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -271,3 +271,4 @@ test('T12938', normal, compile, [''])
 test('T14131', normal, compile, [''])
 test('T14162', normal, compile, [''])
 test('T14237', normal, compile, [''])
+test('T14554', normal, compile, [''])