diff options
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 31 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T12734.hs | 92 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T12734a.hs | 104 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T12734a.stderr | 9 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 2 |
5 files changed, 237 insertions, 1 deletions
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 27529e47f4..6e04e2c29f 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -123,6 +123,7 @@ import qualified TcRnMonad as TcM import qualified TcMType as TcM import qualified TcEnv as TcM ( checkWellStaged, topIdLvl, tcGetDefaultTys, tcLookupClass ) +import PrelNames( heqTyConKey, eqTyConKey ) import Kind import TcType import DynFlags @@ -194,15 +195,37 @@ We can often solve all goals without processing *any* derived constraints. The derived constraints are just there to help us if we get stuck. So we keep them in a separate list. +Note [Prioritise class equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We prioritise equalities in the solver (see selectWorkItem). But class +constraints like (a ~ b) and (a ~~ b) are actually equalities too; +see Note [The equality types story] in TysPrim. + +Failing to prioritise these is inefficient (more kick-outs etc). +But, worse, it can prevent us spotting a "recursive knot" among +Wanted constraints. See comment:10 of Trac #12734 for a worked-out +example. + +So we arrange to put these particular class constraints in the wl_eqs. + + NB: since we do not currently apply the substition to the + inert_solved_dicts, the knot-tying still seems a bit fragile. + But this makes it better. -} -- See Note [WorkList priorities] data WorkList - = WL { wl_eqs :: [Ct] + = WL { wl_eqs :: [Ct] -- Both equality constraints and their + -- class-level variants (a~b) and (a~~b); + -- See Note [Prioritise class equalities] + , wl_funeqs :: [Ct] -- LIFO stack of goals + , wl_rest :: [Ct] + , wl_deriv :: [CtEvidence] -- Implicitly non-canonical -- See Note [Process derived items last] + , wl_implics :: Bag Implication -- See Note [Residual implications] } @@ -260,9 +283,15 @@ extendWorkListCt ct wl | Just (tc,_) <- tcSplitTyConApp_maybe ty1 , isTypeFamilyTyCon tc -> extendWorkListFunEq ct wl + EqPred {} -> extendWorkListEq ct wl + ClassPred cls _ -- See Note [Prioritise class equalites] + | cls `hasKey` heqTyConKey + || cls `hasKey` eqTyConKey + -> extendWorkListEq ct wl + _ -> extendWorkListNonEq ct wl extendWorkListCts :: [Ct] -> WorkList -> WorkList diff --git a/testsuite/tests/typecheck/should_compile/T12734.hs b/testsuite/tests/typecheck/should_compile/T12734.hs new file mode 100644 index 0000000000..a3b26d5aaf --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12734.hs @@ -0,0 +1,92 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} + +--------------- The original bug report -------------- +-- +-- See T12734a for a smaller version + +module T12734 where + +import Prelude +import Control.Applicative +import Control.Monad.Fix +import Control.Monad.Trans.Identity +import Control.Monad.Trans.Class +import Control.Monad.IO.Class + + +data A +data B +data Net +data Type + +data Layer4 t l +data TermStore + +-- Helpers: Stack + +data Stack layers (t :: * -> *) where + SLayer :: t l -> Stack ls t -> Stack (l ': ls) t + SNull :: Stack '[] t + +instance ( Constructor m (t l) + , Constructor m (Stack ls t)) => Constructor m (Stack (l ': ls) t) +instance Monad m => Constructor m (Stack '[] t) + + +-- Helpers: Expr + +newtype Expr t layers = Expr (TermStack t layers) +type TermStack t layers = Stack layers (Layer4 (Expr t layers)) + + +-- Helpers: Funny typeclass + +class Monad m => Constructor m t + +instance ( Monad m, expr ~ Expr t layers, Constructor m (TermStack t layers) + ) => Constructor m (Layer4 expr Type) + + +-- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack overflow +test_gr :: ( Constructor m (TermStack t layers), Inferable A layers m, Inferable B t m + , bind ~ Expr t layers +-- ) => m (Expr t layers) + ) => m bind +test_gr = undefined + + +-- Explicit information about a type which could be inferred + +class Monad m => Inferable (cls :: *) (t :: k) m | cls m -> t + +newtype KnownTypex (cls :: *) (t :: k) (m :: * -> *) (a :: *) = KnownTypex (IdentityT m a) deriving (Show, Functor, Monad, MonadIO, MonadFix, MonadTrans, Applicative, Alternative) + +instance {-# OVERLAPPABLE #-} (t ~ t', Monad m) => Inferable cls t (KnownTypex cls t' m) +instance {-# OVERLAPPABLE #-} (Inferable cls t n, MonadTrans m, Monad (m n)) => Inferable cls t (m n) + + +runInferenceTx :: forall cls t m a. KnownTypex cls t m a -> m a +runInferenceTx = undefined + + + +-- running it + +test_ghc_err :: (MonadIO m, MonadFix m) + => m (Expr Net '[Type]) +test_ghc_err = runInferenceTx @B @Net + $ runInferenceTx @A @'[Type] + $ (test_gr) diff --git a/testsuite/tests/typecheck/should_compile/T12734a.hs b/testsuite/tests/typecheck/should_compile/T12734a.hs new file mode 100644 index 0000000000..01ae2a6255 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12734a.hs @@ -0,0 +1,104 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} + + +-- This version is shorter than T12734, and should yield a +-- type error message. If things go wrong, you get +-- an nfinite loop + +module T12734a where + +import Prelude +import Control.Applicative +import Control.Monad.Fix +import Control.Monad.Trans.Identity +import Control.Monad.Trans.Class +import Control.Monad.IO.Class + + +data A +data B +data Net +data Type + +data Layer4 t l +data TermStore + +data Stack lrs (t :: * -> *) where + SLayer :: t l -> Stack ls t -> Stack (l ': ls) t + SNull :: Stack '[] t + +instance ( Con m (t l) + , Con m (Stack ls t)) => Con m (Stack (l ': ls) t) +instance Monad m => Con m (Stack '[] t) +instance ( expr ~ Expr t lrs + , Con m (TStk t lrs)) => Con m (Layer4 expr Type) + + +newtype Expr t lrs = Expr (TStk t lrs) +type TStk t lrs = Stack lrs (Layer4 (Expr t lrs)) + + +class Con m t + + +-- HERE IS A FUNNY BEHAVIOR: the commented line raises context reduction stack overflow +test_gr :: forall m t lrs bind. + ( Con m (TStk t lrs) + , bind ~ Expr t lrs +-- ) => m (Expr t lrs) -- GHC 8 worked if you said this... + ) => m bind -- but not this! +test_gr = undefined + + +newtype KT (cls :: *) (t :: k) (m :: * -> *) (a :: *) + = KT (IdentityT m a) + +test_ghc_err :: KT A '[Type] IO (Expr Net '[Type]) + +test_ghc_err = test_gr @(KT A '[Type] IO) @_ @'[Type] @(Expr Net '[Type]) + +{- Works! +test_ghc_err = test_gr @(KT A '[Type] IO) + @Net + @'[Type] + @(Expr Net '[Type]) +-} + +{- Some notes. See comment:10 on Trac #12734 + +[W] Con m (TStk t lrs) +[W] Inferable A lrs m +[W] bind ~ Expr t lrs +[W] m bind ~ KT A '[Type] IO (Expr Net '[Type]) + +==> m := KT A '[Type] IO + bind := Expr Net '[Type] + t := Net + lrs := '[Type] + +[W] Con m (TStk t lrs) + = Con m (Stack lrs (Layer4 bind)) +--> inline lrs +[W] Con m (Stack '[Type] (Layer4 bind)) +--> isntance +[W] Con m (Stack '[] bind) + --> Monad m ++ +[W] Con m (Layer4 bind Type) +--> +[W] bind ~ Expr t0 lrs0 +[W] Con m (TStk t0 lrs0) +-} diff --git a/testsuite/tests/typecheck/should_compile/T12734a.stderr b/testsuite/tests/typecheck/should_compile/T12734a.stderr new file mode 100644 index 0000000000..737659fa57 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12734a.stderr @@ -0,0 +1,9 @@ + +T12734a.hs:71:16: error: + • No instance for (Monad (KT A '[Type] IO)) + arising from a use of ‘test_gr’ + • In the expression: + test_gr @(KT A '[Type] IO) @_ @'[Type] @(Expr Net '[Type]) + In an equation for ‘test_ghc_err’: + test_ghc_err + = test_gr @(KT A '[Type] IO) @_ @'[Type] @(Expr Net '[Type]) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 3961b23720..67debd4f1a 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -548,3 +548,5 @@ test('T12644', normal, compile, ['']) test('T12427a', normal, compile_fail, ['']) test('T12427b', normal, compile, ['']) test('T12507', normal, compile, ['']) +test('T12734', normal, compile, ['']) +test('T12734a', normal, compile_fail, ['']) |