Prioritise class-level equality costraints
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 24 Oct 2016 15:55:49 +0000 (16:55 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 24 Oct 2016 15:55:49 +0000 (16:55 +0100)
This patch fixes Trac #12734 by prioritising the class-level
variants of equality constraints, namely (a~b) and (a~~b).

See comment:10 of Trac #12734 for a description of what
went wrong, and Note [Prioritise class equalities] in TcSMonad.

The fix is still not great, but it's a definite step forward, and
cures the particular problem.

Worth merging to 8.0.

compiler/typecheck/TcSMonad.hs
testsuite/tests/typecheck/should_compile/T12734.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T12734a.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/T12734a.stderr [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index 27529e4..6e04e2c 100644 (file)
@@ -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 (file)
index 0000000..a3b26d5
--- /dev/null
@@ -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 (file)
index 0000000..01ae2a6
--- /dev/null
@@ -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 (file)
index 0000000..737659f
--- /dev/null
@@ -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])
index 3961b23..67debd4 100644 (file)
@@ -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, [''])