+import GHC.Core.TyCo.Compare( eqType, eqTypeX, eqTypeIgnoringMultiplicity )

+    warnPprTrace (not (coercionLKind co `eqTypeIgnoringMultiplicity` exprType expr)) "Bad cast"

+{-# LANGUAGE TypeFamilies        #-}

+        literalToPmLit, negatePmLit,

+import GHC.Core.TyCo.Compare( eqType, nonDetCmpType )

+

+import Data.List( find )

+import qualified Data.Map as FM

+import qualified Data.Semigroup as S

+

+{- *********************************************************************

+*                                                                      *

+                 PmLit and PmLitValue

+*                                                                      *

+********************************************************************* -}

+

+       -- We won't actually see PmLitString in the oracle

+       -- since we desugar strings to lists

+

+  -- Overloaded literals

+-- | Syntactic equality.

+-- We want (Ord PmLit) so that we can use (Map PmLit x) in `PmAltConSet`

+instance Eq PmLit where

+  a == b = (a `compare` b) == EQ

+instance Ord PmLit where

+  compare = cmpPmLit

+

+cmpPmLit :: PmLit -> PmLit -> Ordering

+-- This function does "syntactic comparison":

+--   For overloaded literals, compare the type and value

+--   For non-overloaded literals, just compare the values

+-- But it treats (say)

+--    (PmLit Bool (PmLitOverInt 1))

+--    (PmLit Bool (PmLitOverInt 2))

+-- as un-equal, even through (fromInteger @Bool 1)

+-- could be the same as (fromInteger @Bool 2)

+cmpPmLit (PmLit { pm_lit_ty = t1, pm_lit_val = val1 })

+         (PmLit { pm_lit_ty = t2, pm_lit_val = val2 })

+  = case (val1,val2) of

+      (PmLitInt i1, PmLitInt i2) -> i1 `compare` i2

+      (PmLitRat r1, PmLitRat r2) -> r1 `compare` r2

+      (PmLitChar c1, PmLitChar c2) -> c1 `compare` c2

+      (PmLitString s1, PmLitString s2) -> s1 `uniqCompareFS` s2

+      (PmLitOverInt n1 i1, PmLitOverInt n2 i2) -> (n1 `compare` n2) S.<>

+                                                  (i1 `compare` i2) S.<>

+                                                  (t1 `nonDetCmpType` t2)

+      (PmLitOverRat n1 r1, PmLitOverRat n2 r2) -> (n1 `compare` n2) S.<>

+                                                  (r1 `compare` r2) S.<>

+                                                  (t1 `nonDetCmpType` t2)

+      (PmLitOverString s1, PmLitOverString s2) -> (s1 `uniqCompareFS` s2) S.<>

+                                                  (t1 `nonDetCmpType` t2)

+      (PmLitInt {},    _) -> LT

+      (PmLitRat {},    PmLitInt {})  -> GT

+      (PmLitRat {},    _)            -> LT

+      (PmLitChar {},   PmLitInt {})  -> GT

+      (PmLitChar {},   PmLitRat {})  -> GT

+      (PmLitChar {},   _)            -> LT

+      (PmLitString {}, PmLitInt {})  -> GT

+      (PmLitString {}, PmLitRat {})  -> GT

+      (PmLitString {}, PmLitChar {}) -> GT

+      (PmLitString {}, _)            -> LT

+

+      (PmLitOverString {}, _)                 -> GT

+      (PmLitOverRat {},    PmLitOverString{}) -> LT

+      (PmLitOverRat {},    _)                 -> GT

+      (PmLitOverInt {},    PmLitOverString{}) -> LT

+      (PmLitOverInt {},    PmLitOverRat{})    -> LT

+      (PmLitOverInt {},    _)                 -> GT

+

+  | otherwise            = eqPmLitValue v1 v2

+

+eqPmLitValue :: PmLitValue -> PmLitValue -> PmEquality

+eqPmLitValue v1 v2 = go v1 v2

+

+{- *********************************************************************

+*                                                                      *

+                 PmAltCon and PmAltConSet

+*                                                                      *

+********************************************************************* -}

+

+data PmAltConSet = PACS !(UniqDSet ConLike)

+                        !(FM.Map PmLit PmLit)

+-- We use a (FM.Map PmLit PmLit) here, at the cost of requiring an Ord

+-- instance for PmLit, because in extreme cases the set of PmLits can be

+-- very large.  See #26514.

+emptyPmAltConSet = PACS emptyUniqDSet FM.empty

+isEmptyPmAltConSet (PACS cls lits)

+  = isEmptyUniqDSet cls && FM.null lits

+elemPmAltConSet (PmAltLit lit)    (PACS _   lits) = isJust (FM.lookup lit lits)

+  = PACS cls (FM.insert lit lit lits)

+  = map PmAltConLike (uniqDSetToList cls) ++

+    FM.foldr ((:) . PmAltLit) [] lits

+  = do { (outermost_unif_lvl, better_wc) <- reportCoarseGrainUnifications $

+                                            go_wc False wc

+

+       -- We may have done unifications; if so, solve again

+       ; let unif_happened = not (isInfiniteTcLevel outermost_unif_lvl)

+    go_implic encl_eqs implic@(Implic { ic_tclvl = tclvl

+                                      , ic_status = status, ic_wanted = wanteds

+                                      , ic_given_eqs = given_eqs, ic_binds = binds })

+           ; wanteds' <- setTcLevelTcS tclvl $

+                         -- Set the levels so that reportCoarseGrainUnifications works

+                         setEvBindsTcS binds $

+  neither is more general than the other.   But by the time defaulting takes

+  place all let-bound variables have got their final types; defaulting won't

+  affect let-generalisation.

+reportCoarseGrainUnifications :: TcS a -> TcS (TcLevel, a)

+-- Specifically: return the TcLevel of the outermost (smallest level)

+--   unification variable that has been unified, or infiniteTcLevel if none

+      WU_None -> report_coarse_grain_unifs env thing_inside

+        -> do { (inner_ul, res) <- report_coarse_grain_unifs env thing_inside

+                     , text "inner_ul" <+> ppr inner_ul]

+              ; return (inner_ul, res) }

+

+              -- Propagate to outer_tvs_rev

+              ; TcM.updTcRef outer_tvs_ref (`unionVarSet` unif_tvs)

+

+              ; let outermost_unif_lvl = minTcTyVarSetLevel unif_tvs

+                     , text "unif_happened" <+> ppr outermost_unif_lvl ]

+              ; return (outermost_unif_lvl, res) }

+                          -> TcM (TcLevel, a)

+-- Returns the level number of the outermost

+-- unification variable that is unified

+       ; inner_ul <- TcM.readTcRef inner_ul_ref

+       ; TcM.traceTc "report_coarse" $

+         text "inner_lvl ="   <+> ppr inner_ul

+       ; return (inner_ul, res) }

+       ; ambient_lvl <- getTcLevel

+       ; (simple_unif_lvl, wc1)

+       ; let simple_unif_happened = ambient_lvl `deeperThanOrSame` simple_unif_lvl

+       ; (implic_unif_lvl, implics')

+                then return (infiniteTcLevel, implics)

+         -- unification, hence looking only at `implic_unif_lvl`.  (Even if the

+         -- /simples/ did unifications we don't need to re-do them.)

+         -- Also note that we only iterate if `implic_unify_lvl` is /equal to/

+         -- the current level; if it is less , we'll iterate some outer level,

+         -- which will bring us back here anyway.

+         -- See Note [When to iterate the solver: unifications]

+       ; let implic_unif_happened = implic_unif_lvl `sameDepthAs` ambient_lvl

+       ; csTraceTcS $ text "implic_unif_happened" <+> ppr implic_unif_happened

+       ; maybe_simplify_again (n+1) limit implic_unif_happened wc' }

+maybe_simplify_again :: Int -> IntWithInf

+                     -> Bool   -- True <=> Solving the implications did some unifications

+                               --          at the current level; so iterate

+Hence the `definitely_redo_implications` flag to `simplify_loop`.  It's usually True,

+but False in the case where the only reason to iterate is new Wanted superclasses.

+In that case we check whether the new Wanteds actually led to any new unifications

+(at all), and iterate the implications only if so.

+  infiniteTcLevel, isInfiniteTcLevel,

+isInfiniteTcLevel :: TcLevel -> Bool

+isInfiniteTcLevel QLInstVar = True

+isInfiniteTcLevel _         = False

+

+  -- Eq and Ord instances are done explicitly

+{-# LANGUAGE MagicHash #-}

+

+module Main where

+

+import GHC.Exts ( Int# )

+

+expensive :: Int -> Int#

+expensive 0 = 2#

+expensive i = expensive (i-1)

+

+data D = MkD Int# Int

+

+f :: a -> Bool

+f _ = False

+{-# NOINLINE f #-}

+

+{-# RULES "f/MkD" forall x. f (MkD x) = True #-}

+

+bar :: Bool

+bar = f (MkD (expensive 10))

+

+main :: IO ()

+main = print bar

+True

+test('T26311', normal, compile_and_run, ['-O1'])

+        Patterns of type ‘a’ not matched: p where p is not one of {1, 2, 3}

+

+{-# LANGUAGE AllowAmbiguousTypes #-}

+{-# LANGUAGE BangPatterns #-}

+{-# LANGUAGE BlockArguments #-}

+{-# LANGUAGE DataKinds #-}

+{-# LANGUAGE MagicHash #-}

+{-# LANGUAGE PolyKinds #-}

+{-# LANGUAGE ScopedTypeVariables #-}

+{-# LANGUAGE StandaloneKindSignatures #-}

+{-# LANGUAGE TypeApplications #-}

+{-# LANGUAGE TypeFamilies #-}

+{-# LANGUAGE UnboxedTuples #-}

+

+module T26072b where

+

+-- base

+import Data.Kind

+import GHC.TypeNats

+import GHC.Exts

+  ( TYPE, RuntimeRep(..), LiftedRep

+  , proxy#

+  )

+

+--------------------------------------------------------------------------------

+

+-- Stub for functions in 'primitive' (to avoid dependency)

+type PrimArray :: Type -> Type

+data PrimArray a = MkPrimArray

+

+indexPrimArray :: PrimArray a -> Int -> a

+indexPrimArray _ _ = error "unimplemented"

+{-# NOINLINE indexPrimArray #-}

+

+--------------------------------------------------------------------------------

+

+int :: forall n. KnownNat n => Int

+int = fromIntegral ( natVal' @n proxy# )

+

+type Fin :: Nat -> Type

+newtype Fin n = Fin { getFin :: Int }

+

+-- Vector

+type V :: Nat -> Type -> Type

+newtype V n a = V ( PrimArray a )

+

+-- Matrix

+type M :: Nat -> Type -> Type

+newtype M n a = M ( PrimArray a )

+

+type IndexRep :: (Type -> Type) -> RuntimeRep

+type family IndexRep f

+class Ix f where

+  type Index f :: TYPE (IndexRep f)

+  (!) :: f a -> Index f -> a

+  infixl 9 !

+

+type instance IndexRep ( V n ) = LiftedRep

+instance Ix ( V n ) where

+  type Index ( V n ) = Fin n

+  V v ! Fin !i = indexPrimArray v i

+  {-# INLINE (!) #-}

+

+type instance IndexRep ( M m ) = TupleRep [ LiftedRep, LiftedRep ]

+

+instance KnownNat n => Ix ( M n ) where

+  type Index ( M n ) = (# Fin n, Fin n #)

+  M m ! (# Fin !i, Fin !j #) = indexPrimArray m ( i + j * int @n )

+  {-# INLINE (!) #-}

+

+rowCol :: forall n a. ( KnownNat n, Num a ) => Fin n -> M n a -> V n a -> a

+rowCol i m v = go 0 ( Fin 0 )

+  where

+    n = int @n

+    go :: a -> Fin n -> a

+    go !acc j@( Fin !j_ )

+      | j_ >= n

+      = acc

+      | otherwise

+      = go ( acc + m ! (# i , j #) * v ! j ) ( Fin ( j_ + 1 ) )

+test('T26072b', js_broken(26578), compile, [''])                             ##

+{-# LANGUAGE GADTs #-}

+

+module T26582 where

+

+sametype :: a -> a -> Int

+sametype = sametype

+

+f :: Eq a => (a->Int) -> Int

+f = f

+

+data T b where T1 :: T Bool

+

+g1 :: T b -> Int

+g1 v = f (\x -> case v of { T1 -> sametype x True })

+

+g2 :: Eq c => c -> T b -> Int

+g2 c v = f (\x -> case v of { T1 -> sametype x c })

+

+{- The point is that we get something like

+

+     Wanted: [W] d : Eq alpha[1]

+     Implication

+       level:  2

+       Given:  b~Bool

+

+       Wanted: [W] alpha[1]~Bool       -- For g1

+       Wanted: [W] alpha[1]~c          -- For g2

+

+So alpha is untouchable under the (b~Bool) from the GADT.

+And yet in the end it's easy to solve

+via alpha:=Bool, or alpha:=c resp

+

+But having done that defaulting we must then remember to

+solved that `d : Eq alpha`!  We forgot to so so in #26582.

+-}

+test('T26582', normal, compile, [''])