[commit: ghc] master: Don't deeply expand insolubles (74cd1be)

[git at git.haskell.org]

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

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

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

commit 74cd1be0b2778ad99566cde085328bde2090294a
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Oct 17 16:30:33 2017 +0100

    Don't deeply expand insolubles
    
    Trac #13450 went bananas if we expand insoluble constraints.
    Better just to leave them un-expanded.
    
    I'm not sure in detail about why it goes so badly wrong; but
    regardless, the less we mess around with insoluble contraints
    the better the error messages will be.


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

74cd1be0b2778ad99566cde085328bde2090294a
 compiler/typecheck/TcCanonical.hs               | 22 ++++++---
 testsuite/tests/typecheck/should_fail/T14350.hs | 59 +++++++++++++++++++++++++
 testsuite/tests/typecheck/should_fail/all.T     |  1 +
 3 files changed, 76 insertions(+), 6 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 8d4d2a0..39f2def 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -86,7 +86,7 @@ canonicalize (CNonCanonical { cc_ev = ev })
       EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
                                   canEqNC    ev eq_rel ty1 ty2
       IrredPred {}          -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
-                                  canIrred   ev
+                                  canIrred ev
 
 canonicalize (CIrredCan { cc_ev = ev })
   = canIrred ev
@@ -486,17 +486,27 @@ mk_strict_superclasses rec_clss ev cls tys
 
 canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
 -- Precondition: ty not a tuple and no other evidence form
-canIrred old_ev
-  = do { let old_ty = ctEvPred old_ev
-       ; traceTcS "can_pred" (text "IrredPred = " <+> ppr old_ty)
-       ; (xi,co) <- flatten FM_FlattenAll old_ev old_ty -- co :: xi ~ old_ty
-       ; rewriteEvidence old_ev xi co `andWhenContinue` \ new_ev ->
+canIrred ev
+  | EqPred eq_rel ty1 ty2 <- classifyPredType pred
+  = -- For insolubles (all of which are equalities, do /not/ flatten the arguments
+    -- In Trac #14350 doing so led entire-unnecessary and ridiculously large
+    -- type function expansion.  Instead, canEqNC just applies
+    -- the substitution to the predicate, and may do decomposition;
+    --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
+    canEqNC ev eq_rel ty1 ty2
+
+  | otherwise
+  = do { traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
+       ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
+       ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
     do { -- Re-classify, in case flattening has improved its shape
        ; case classifyPredType (ctEvPred new_ev) of
            ClassPred cls tys     -> canClassNC new_ev cls tys
            EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
            _                     -> continueWith $
                                     mkIrredCt new_ev } }
+  where
+    pred = ctEvPred ev
 
 canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
 canHole ev hole
diff --git a/testsuite/tests/typecheck/should_fail/T14350.hs b/testsuite/tests/typecheck/should_fail/T14350.hs
new file mode 100644
index 0000000..b3de40f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T14350.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T14350 where
+
+import Data.Kind
+
+data Proxy a = Proxy
+data family Sing (a :: k)
+
+data SomeSing k where
+  SomeSing :: Sing (a :: k) -> SomeSing k
+
+class SingKind k where
+  type Demote k :: Type
+  fromSing :: Sing (a :: k) -> Demote k
+  toSing   :: Demote k -> SomeSing k
+
+data instance Sing (x :: Proxy k) where
+  SProxy :: Sing 'Proxy
+
+instance SingKind (Proxy k) where
+  type Demote (Proxy k) = Proxy k
+  fromSing SProxy = Proxy
+  toSing Proxy = SomeSing SProxy
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type a @@ b = Apply a b
+infixl 9 @@
+
+newtype instance Sing (f :: k1 ~> k2) =
+  SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
+
+instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
+  type Demote (k1 ~> k2) = Demote k1 -> Demote k2
+  fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y)
+  toSing = undefined
+
+dcomp :: forall (a :: Type)
+                (b :: a ~> Type)
+                (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
+                (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
+                (g :: forall (x :: a). Proxy x ~> b @@ x)
+                (x :: a).
+         Sing f
+      -> Sing g
+      -> Sing x
+      -> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
+dcomp f g x = applySing f Proxy Proxy
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 381e2c5..1aa23c4 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -459,3 +459,4 @@ test('T13909', normal, compile_fail, [''])
 test('T13929', normal, compile_fail, [''])
 test('T14232', normal, compile_fail, [''])
 test('T14325', normal, compile_fail, [''])
+test('T14350', normal, compile_fail, [''])