Commit 74cd1be0 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 317aa966
......@@ -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
......
{-# 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
......@@ -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, [''])
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