Commit 1132ec68 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

Fix a nasty bug in the pure unifier

The pure unifier was building an infinite type, through a defective
occurs check.  So GHC went into an infinite loop.

Reason: we were neglecting the 'kco' part of the type, which
'unify_ty' maintains.  Yikes.

The fix is easy.  I refactored a bit to make it harder to
go wrong in future.

(cherry picked from commit e99fdf77)
parent d8dbe293
......@@ -1001,11 +1001,9 @@ uUnrefined env tv1 ty2 ty2' kco
b2 = tvBindFlagR env tv2
ty1 = mkTyVarTy tv1
; case (b1, b2) of
(BindMe, _) -> do { checkRnEnvR env ty2 -- make sure ty2 is not a local
; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
(BindMe, _) -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
(_, BindMe) | um_unif env
-> do { checkRnEnvL env ty1 -- ditto for ty1
; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
-> bindTv (umSwapRn env) tv2 (ty1 `mkCastTy` kco)
_ | tv1' == tv2' -> return ()
-- How could this happen? If we're only matching and if
......@@ -1014,25 +1012,36 @@ uUnrefined env tv1 ty2 ty2' kco
_ -> maybeApart -- See Note [Unification with skolems]
}}}}
uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable
= do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
; if um_unif env && occurs -- See Note [Self-substitution when matching]
then maybeApart -- Occurs check, see Note [Fine-grained unification]
else bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) }
-- Bind tyvar to the synonym if poss
uUnrefined env tv1 ty2 _ kco -- ty2 is not a type variable
= case tvBindFlagL env tv1 of
Skolem -> maybeApart -- See Note [Unification with skolems]
BindMe -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
elemNiSubstSet v set
bindTv :: UMEnv -> TyVar -> Type -> UM ()
-- OK, so we want to extend the substitution with tv := ty
-- But first, we must do a couple of checks
bindTv env tv1 ty2
= do { let free_tvs2 = tyCoVarsOfType ty2
-- Make sure tys mentions no local variables
-- E.g. (forall a. b) ~ (forall a. [a])
-- We should not unify b := [a]!
; checkRnEnvR env free_tvs2
-- Occurs check, see Note [Fine-grained unification]
; occurs <- occursCheck env tv1 free_tvs2
; if occurs then maybeApart
else extendTvEnv tv1 ty2 }
occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
occursCheck env tv free_tvs
| um_unif env
= do { tsubst <- getTvSubstEnv
; return $ v `elemVarSet` niSubstTvSet tsubst set }
; return (tv `elemVarSet` niSubstTvSet tsubst free_tvs) }
bindTv :: UMEnv -> TyVar -> Type -> UM ()
bindTv env tv ty -- ty is not a variable
= do { checkRnEnvR env ty -- make sure ty mentions no local variables
; case tvBindFlagL env tv of
Skolem -> maybeApart -- See Note [Unification with skolems]
BindMe -> extendTvEnv tv ty
}
| otherwise -- Matching; no occurs check
= return False -- See Note [Self-substitution when matching]
{-
%************************************************************************
......@@ -1149,7 +1158,8 @@ checkRnEnv get_set env varset = UM $ \ state ->
-- means we don't have to calculate the free vars of
-- the type, often saving quite a bit of allocation.
then Unifiable (state, ())
else MaybeApart (state, ())
else MaybeApart (state, ()) -- ToDo: why MaybeApart
-- I think SurelyApart would be right
-- | Converts any SurelyApart to a MaybeApart
don'tBeSoSure :: UM () -> UM ()
......@@ -1158,11 +1168,8 @@ don'tBeSoSure um = UM $ \ state ->
SurelyApart -> MaybeApart (state, ())
other -> other
checkRnEnvR :: UMEnv -> Type -> UM ()
checkRnEnvR env ty = checkRnEnv rnEnvR env (tyCoVarsOfType ty)
checkRnEnvL :: UMEnv -> Type -> UM ()
checkRnEnvL env ty = checkRnEnv rnEnvL env (tyCoVarsOfType ty)
checkRnEnvR :: UMEnv -> VarSet -> UM ()
checkRnEnvR env fvs = checkRnEnv rnEnvR env fvs
checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
......
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module T14846 where
import Data.Kind
import Data.Proxy
type Cat ob = ob -> ob -> Type
data Struct :: (k -> Constraint) -> Type where
S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls -> Type where
AStruct :: cls a => AStruct (Structured a cls)
class StructI xx (structured::Struct (cls :: k -> Constraint)) where
struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI xx structured where
struct :: AStruct (Structured xx cls)
struct = AStruct
data Hom :: Cat k -> Cat (Struct cls) where
class Category (cat::Cat ob) where
i :: StructI xx a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
i :: forall xx a. StructI xx a => Hom ríki a a
i = case struct :: AStruct (Structured a cls) of
T14846.hs:38:8: error:
• Couldn't match kind ‘cls1’ with ‘cls0’
‘cls1’ is a rigid type variable bound by
the type signature for:
i :: forall k5 (cls1 :: k5
-> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki1 :: Struct
cls1
-> Struct
cls1
-> *).
StructI xx a =>
ríki1 a a
at T14846.hs:38:8-48
When matching types
a0 :: Struct cls0
a :: Struct cls1
Expected type: ríki1 a a
Actual type: Hom ríki a0 a0
• When checking that instance signature for ‘i’
is more general than its signature in the class
Instance sig: forall (xx :: k0) (a :: Struct cls0).
StructI xx a =>
Hom ríki a a
Class sig: forall k1 (cls :: k1
-> Constraint) k2 (xx :: k2) (a :: Struct
cls) (ríki :: Struct
cls
-> Struct
cls
-> *).
StructI xx a =>
ríki a a
In the instance declaration for ‘Category (Hom ríki)’
T14846.hs:39:44: error:
• Expected kind ‘Struct cls0 -> Constraint’,
but ‘cls’ has kind ‘k4 -> Constraint’
• In the second argument of ‘Structured’, namely ‘cls’
In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
In an expression type signature: AStruct (Structured a cls)
• Relevant bindings include
i :: Hom ríki a a (bound at T14846.hs:39:3)
......@@ -178,4 +178,5 @@ test('T11203', normal, compile_fail, [''])
test('T14555', normal, compile_fail, [''])
test('T14563', normal, compile_fail, [''])
test('T14723', normal, compile, [''])
test('T14846', normal, compile_fail, [''])
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