Commit b1ea0475 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 6f6d1050
......@@ -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
......
{-# 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
......@@ -271,3 +271,4 @@ test('T12938', normal, compile, [''])
test('T14131', normal, compile, [''])
test('T14162', normal, compile, [''])
test('T14237', normal, compile, [''])
test('T14554', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment