{-# LANGUAGE CPP #-}

{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE MultiWayIf          #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ViewPatterns        #-}

{-|
Module: GHC.TcPlugin.API.TyConSubst

This module provides functionality for recognising whether a type is a
'TyConApp' while taking into account Given nominal equalities.

In particular, this allows dealing with flattening variables on older GHC versions
(9.0 and below). For example, instead of @[W] m + n ~ n + m@, older GHCs might
produce @[G] u ~ m + n, [G] v ~ n + m, [W] u ~ v@. In this case, one needs to
use the Givens to recognise that @u ~ v@ can be solved using the laws of natural
number arithmetic.

Usage:

  - Use 'mkTyConSubst' to create a 'TyConSubst' from Givens.
  - Use 'splitTyConApp_upTo' to compute whether a type is a 'TyConApp', taking
    into account Given constraints (in the form of the 'TyConSubst').

Notes:

  - 'splitTyConApp_upTo' will also look through type synonyms,
  - 'splitTyConApp_upTo' only takes into account nominal equalities.
    Please open a ticket if you have a need for rewriting modulo representational
    equalities.

-}
module GHC.TcPlugin.API.TyConSubst (
    TyConSubst -- opaque

  , mkTyConSubst
  , splitTyConApp_upTo
  ) where

-- Word64Map is available:

--

--  - from 9.10.1 onwards

--  - in 9.8.4

--  - in 9.6.7

--

-- This is unusual: whether a module is exposed depends on the MINOR version

#define HAS_WORD64MAP \
    (MIN_VERSION_ghc(9,9,0) || \
    (MIN_VERSION_ghc(9,8,4) && !(MIN_VERSION_ghc(9,9,0))) || \
    (MIN_VERSION_ghc(9,6,7) && !(MIN_VERSION_ghc(9,7,0))))

-- base

import Data.Bifunctor
  ( Bifunctor(first, second) )
import Data.Either
  ( partitionEithers )
import Data.Foldable
  ( toList, asum )
import Data.List.NonEmpty
  ( NonEmpty(..) )
import Data.Maybe
  ( fromJust )
#if !MIN_VERSION_ghc(8,11,0)
import Unsafe.Coerce
  ( unsafeCoerce )
#endif

-- containers

import Data.Sequence
  ( Seq )
import qualified Data.Sequence as Seq

-- ghc

#if HAS_WORD64MAP
import qualified GHC.Data.Word64Map.Strict as Word64Map
#else
import qualified Data.IntMap.Strict as IntMap
#endif
import GHC.Types.Unique
  ( Uniquable, getUnique )
import qualified GHC.Types.Unique.FM as UFM
import GHC.Types.Unique.Set
  ( UniqSet )
import qualified GHC.Types.Unique.Set as UniqSet
import GHC.Utils.Outputable
  hiding ( (<>) )

-- ghc-tcplugin-api

import GHC.TcPlugin.API
import GHC.Tc.Types.Constraint

{-------------------------------------------------------------------------------
  The main type

  TODO: maybe this could be sped up with
  <https://hackage.haskell.org/package/union-find>?
-------------------------------------------------------------------------------}

-- | Substitution for recognizing 'TyCon' applications modulo nominal equalities.

data TyConSubst = TyConSubst {
      TyConSubst -> UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap :: UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
    , TyConSubst -> UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon :: UniqFM TcTyVar (TcTyVar, [Coercion])
    }
-- During constraint solving the set of Given constraints includes so-called

-- "canonical equalities": equalities of the form

--

-- > var ~ typ                  (CTyEqCan)

-- > var ~ TyCon arg1 .. argN   (CFunEqCan, the TyCon will be a type family)

--

-- The problem we want to solve is recognizing if some type τ is of the form

--

-- > TyCon arg1 arg2 .. argN   (0 <= N)

--

-- modulo those canonical equalities. We limit the scope of what we try to do:

--

-- o We are only interested in recognizing types of the form above

--   (as opposed to general parsing-modulo-equalities).

-- o We will only use the canonical equalities as-is: we will not attempt to

--   derive any additional equalities from them (i.e. if, say, we know that

--   @x ~ T1@ and @x ~ T2@, we will not attempt to use the fact that this means

--   that @T1 ~ T2@, nor any derived conclusions thereof). We /will/ however

--   try to apply the canonical equalities as often as is necessary (e.g.,

--   first applying @x ~ T y@, then applying @y ~ T2@).

--

-- We solve this problem by constructing a 'TyConSubst': a possibly

-- non-deterministic substitution mapping type variables to types of the form

-- above (that is, a type constructor applied to some arguments).

--

-- We detail the construction of this substitution below (see documentation of

-- 'Classified' and 'process'), but once we have this substitution, the

-- recognition problem becomes easy:

--

-- 1. Without loss of generality, let τ be of the form @t arg1 arg2 .. argN@

-- 2. If @t@ is a 'TyCon', we're done.

-- 3. Otherwise, if @t@ is a variable @x@, lookup @x@ in the substitution; if

--    there is one (or more) mappings for @x@, then we have successfully

--    recognized τ to be of the form above. There is no need to apply the

--    substitution repeatedly.

--

-- The substitution is non-deterministic because there might be multiple

-- matches. For example, if we have

--

-- > type family Foo where

-- >   Foo = Int

--

-- then we might well have equalities @x ~ Int, x ~ Foo@ in scope, and so a type

-- @x@ would match two different 'TyCon's. What we do know, however, is that if

-- τ matches both @t arg1 .. argN@ and @t' arg1' .. argM'@ (possibly @N /= M@),

-- then

--

-- > t arg1 .. argN ~ t' arg1' .. argM'

--

-- If @t == t'@, we can conclude that the arguments are equal only if @t@ is

-- injective.


{-------------------------------------------------------------------------------
  Basic functionality for working with 'TyConSubst'
-------------------------------------------------------------------------------}

-- | Empty substitution

--

-- The canonical variables map is established once when the initial substitution

-- is generated and not updated thereafter.

tyConSubstEmpty :: UniqFM TcTyVar (TcTyVar, [Coercion]) -> TyConSubst
tyConSubstEmpty :: UniqFM TcTyVar (TcTyVar, [Coercion]) -> TyConSubst
tyConSubstEmpty UniqFM TcTyVar (TcTyVar, [Coercion])
canon = TyConSubst {
      tyConSubstMap :: UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap   = UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
forall key elt. UniqFM key elt
UFM.emptyUFM
    , tyConSubstCanon :: UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon = UniqFM TcTyVar (TcTyVar, [Coercion])
canon
    }

-- | Lookup a variable in the substitution

tyConSubstLookup :: TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstLookup :: TcTyVar
-> TyConSubst -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstLookup TcTyVar
var TyConSubst{UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: TyConSubst -> UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: TyConSubst -> UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: UniqFM TcTyVar (TcTyVar, [Coercion])
..} =
  ((TyCon, [Type], [Coercion]) -> (TyCon, [Type], [Coercion]))
-> NonEmpty (TyCon, [Type], [Coercion])
-> NonEmpty (TyCon, [Type], [Coercion])
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ( \ (TyCon
tc, [Type]
tys, [Coercion]
deps) -> (TyCon
tc, [Type]
tys, [Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps')) (NonEmpty (TyCon, [Type], [Coercion])
 -> NonEmpty (TyCon, [Type], [Coercion]))
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
-> TcTyVar -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall key elt. Uniquable key => UniqFM key elt -> key -> Maybe elt
UFM.lookupUFM UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap TcTyVar
var'
  where
    var' :: TcTyVar
    deps' :: [Coercion]
    (TcTyVar
var', [Coercion]
deps') = UniqFM TcTyVar (TcTyVar, [Coercion])
-> TcTyVar -> (TcTyVar, [Coercion])
forall a l.
(Uniquable a, Monoid l) =>
UniqFM a (a, l) -> a -> (a, l)
canonicalize UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon TcTyVar
var

-- | Extend substitution with new bindings

tyConSubstExtend ::
     [(TcTyVar, (TyCon, [Type]), [Coercion])]
  -> TyConSubst -> TyConSubst
tyConSubstExtend :: [(TcTyVar, (TyCon, [Type]), [Coercion])]
-> TyConSubst -> TyConSubst
tyConSubstExtend [(TcTyVar, (TyCon, [Type]), [Coercion])]
new subst :: TyConSubst
subst@TyConSubst{UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: TyConSubst -> UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: TyConSubst -> UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: UniqFM TcTyVar (TcTyVar, [Coercion])
..} = TyConSubst
subst {
      tyConSubstMap = UFM.plusUFM_C (<>)
                        (UFM.listToUFM $ map aux new)
                        tyConSubstMap
    }
  where
    aux :: (TcTyVar,          (TyCon, [Type]), [Coercion])
        -> (TcTyVar, NonEmpty (TyCon, [Type] , [Coercion]))
    aux :: (TcTyVar, (TyCon, [Type]), [Coercion])
-> (TcTyVar, NonEmpty (TyCon, [Type], [Coercion]))
aux (TcTyVar
var, (TyCon
tc, [Type]
args), [Coercion]
deps) =
      let (TcTyVar
var', [Coercion]
deps') = UniqFM TcTyVar (TcTyVar, [Coercion])
-> TcTyVar -> (TcTyVar, [Coercion])
forall a l.
(Uniquable a, Monoid l) =>
UniqFM a (a, l) -> a -> (a, l)
canonicalize UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon TcTyVar
var
      in  (TcTyVar
var', (TyCon
tc, [Type]
args, [Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps') (TyCon, [Type], [Coercion])
-> [(TyCon, [Type], [Coercion])]
-> NonEmpty (TyCon, [Type], [Coercion])
forall a. a -> [a] -> NonEmpty a
:| [])

{-------------------------------------------------------------------------------
  Classification
-------------------------------------------------------------------------------}

-- | Classified canonical nominal equality constraints.

--

-- The first step in the construction of the 'TyConSubst' is to classify the

-- available canonical equalities as one of three categories, defined below.

data Classified = Classified {
      -- | " Obviously " productive mappings

      --

      -- An equality @var := TyCon args@ is productive, because as soon as we

      -- apply it, we are done: we have successfully recognized a type as being

      -- an application of a concrete type constructor (note that we only ever

      -- apply the substitution to the head @t@ of a type @t args@, never to the

      -- arguments).

      Classified -> [(TcTyVar, (TyCon, [Type]), [Coercion])]
classifiedProductive :: [(TcTyVar, (TyCon, [Type]), [Coercion])]

      -- | Extend equivalence class of variables

      --

      -- An equality @var1 := var2@ we will regard as extending the equivalence

      -- classes of variables (see 'constructEquivClasses').

    , Classified -> [(TcTyVar, TcTyVar, [Coercion])]
classifiedExtendEquivClass :: [(TcTyVar, TcTyVar, [Coercion])]

      -- | Substitutions we need to reconsider later

      --

      -- An equality @var1 := var2 args@ (with @args@ a non-empty list of

      -- arguments) is most problematic. Applying it /may/ allow us to make

      -- progress, but it may not (consider for example @var := var arg@). We

      -- will reconsider such equalities at the end (see 'process').

    , Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
    }

instance Semigroup Classified where
  Classified
c1 <> :: Classified -> Classified -> Classified
<> Classified
c2 = Classified {
        classifiedProductive :: [(TcTyVar, (TyCon, [Type]), [Coercion])]
classifiedProductive       = (Classified -> [(TcTyVar, (TyCon, [Type]), [Coercion])])
-> [(TcTyVar, (TyCon, [Type]), [Coercion])]
forall a. (Classified -> [a]) -> [a]
combine Classified -> [(TcTyVar, (TyCon, [Type]), [Coercion])]
classifiedProductive
      , classifiedExtendEquivClass :: [(TcTyVar, TcTyVar, [Coercion])]
classifiedExtendEquivClass = (Classified -> [(TcTyVar, TcTyVar, [Coercion])])
-> [(TcTyVar, TcTyVar, [Coercion])]
forall a. (Classified -> [a]) -> [a]
combine Classified -> [(TcTyVar, TcTyVar, [Coercion])]
classifiedExtendEquivClass
      , classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
classifiedReconsider       = (Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])])
-> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
forall a. (Classified -> [a]) -> [a]
combine Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
classifiedReconsider
      }
    where
      combine :: (Classified -> [a]) -> [a]
      combine :: forall a. (Classified -> [a]) -> [a]
combine Classified -> [a]
f = Classified -> [a]
f Classified
c1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Classified -> [a]
f Classified
c2

instance Monoid Classified where
  mempty :: Classified
mempty = [(TcTyVar, (TyCon, [Type]), [Coercion])]
-> [(TcTyVar, TcTyVar, [Coercion])]
-> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
-> Classified
Classified [] [] []

productive :: TcTyVar -> (TyCon, [Type]) -> [Coercion] -> Classified
productive :: TcTyVar -> (TyCon, [Type]) -> [Coercion] -> Classified
productive TcTyVar
var (TyCon, [Type])
app [Coercion]
deps = Classified
forall a. Monoid a => a
mempty {
      classifiedProductive = [(var, app, deps)]
    }

extendEquivClass :: TcTyVar -> TcTyVar -> [Coercion] -> Classified
extendEquivClass :: TcTyVar -> TcTyVar -> [Coercion] -> Classified
extendEquivClass TcTyVar
var TcTyVar
var' [Coercion]
deps = Classified
forall a. Monoid a => a
mempty {
      classifiedExtendEquivClass = [(var, var', deps)]
    }

reconsider :: TcTyVar -> (TcTyVar, NonEmpty Type) -> [Coercion] -> Classified
reconsider :: TcTyVar -> (TcTyVar, NonEmpty Type) -> [Coercion] -> Classified
reconsider TcTyVar
var (TcTyVar
var', NonEmpty Type
args) [Coercion]
deps = Classified
forall a. Monoid a => a
mempty {
      classifiedReconsider = [(var, (var', args), deps)]
    }

-- | Classify a set of Given constraints.

--

-- See 'Classified' for details.

classify :: [Ct] -> Classified
classify :: [Ct] -> Classified
classify = Classified -> [Ct] -> Classified
go Classified
forall a. Monoid a => a
mempty
  where
    go :: Classified -> [Ct] -> Classified
    go :: Classified -> [Ct] -> Classified
go Classified
acc []     = Classified
acc
    go Classified
acc (Ct
c:[Ct]
cs) =
      let deps :: [Coercion]
deps = [HasDebugCallStack => CtEvidence -> Coercion
CtEvidence -> Coercion
ctEvCoercion (Ct -> CtEvidence
ctEvidence Ct
c)] in
        case Ct -> Maybe (TcTyVar, Type, EqRel)
isCanonicalVarEq Ct
c of
          Just (TcTyVar
var, Type -> (Type, [Type])
splitAppTys -> (Type
fn, [Type]
args), EqRel
NomEq)
            | Just (TyCon
tyCon, [Type]
inner) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
fn ->
                Classified -> [Ct] -> Classified
go (TcTyVar -> (TyCon, [Type]) -> [Coercion] -> Classified
productive TcTyVar
var (TyCon
tyCon, [Type]
inner [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args) [Coercion]
deps Classified -> Classified -> Classified
forall a. Semigroup a => a -> a -> a
<> Classified
acc) [Ct]
cs
            | Just TcTyVar
var' <- Type -> Maybe TcTyVar
getTyVar_maybe Type
fn, [Type] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args ->
                Classified -> [Ct] -> Classified
go (TcTyVar -> TcTyVar -> [Coercion] -> Classified
extendEquivClass TcTyVar
var TcTyVar
var' [Coercion]
deps Classified -> Classified -> Classified
forall a. Semigroup a => a -> a -> a
<> Classified
acc) [Ct]
cs
            | Just TcTyVar
var' <- Type -> Maybe TcTyVar
getTyVar_maybe Type
fn, Type
x:[Type]
xs <- [Type]
args ->
                Classified -> [Ct] -> Classified
go (TcTyVar -> (TcTyVar, NonEmpty Type) -> [Coercion] -> Classified
reconsider TcTyVar
var (TcTyVar
var', Type
x Type -> [Type] -> NonEmpty Type
forall a. a -> [a] -> NonEmpty a
:| [Type]
xs) [Coercion]
deps Classified -> Classified -> Classified
forall a. Semigroup a => a -> a -> a
<> Classified
acc) [Ct]
cs
          Maybe (TcTyVar, Type, EqRel)
_otherwise ->
            Classified -> [Ct] -> Classified
go Classified
acc [Ct]
cs

{-------------------------------------------------------------------------------
  Processing
-------------------------------------------------------------------------------}

-- | Construct 'TyCon' substitution from classified nominal equality constraints.

--

-- The difficult part in constructing this substitution are the equalities of

-- the form @var1 ~ var2 args@, which we ear-marked as "to reconsider" during

-- classification.

--

-- We will do this iteratively:

--

-- o We first construct a set of variable equivalence classes based on

--   'classifiedExtendEquivClass' (using 'constructEquivClasses'), and use that

--   along with the "obviously productive" equalities ('classifiedProductive')

--   as the initial value of the accumulator (a 'TyConSubst').

-- o We then repeatedly consider the remaining equalities. Whenever there is

--   a substitution available in the accumulator for @var2@ which turns it into

--   a type of the form @TyCon args'@, we add @var1 := TyCon args' args@ to the

--   accumulator.

-- o We keep doing this until we can make no more progress.

--

-- The functions for working with 'TyConSubst' take the variable equivalence

-- classes into account, so we do not need to do that here.

--

-- Two observations:

--

-- o This process must terminate: there are a finite number of constraints

--   to consider, and whenever we apply a substitution from the accumulator,

--   we get an "obviously productive" substitution: we do not create new work

--   in the loop.

-- o We may end up ignoring some substitutions: if there is a substitution

--   @var1 := var2 args@ and we don't have any (productive) substitutions for

--   @var2@, we will just ignore it.

--

-- A note on recursive bindings: a direct or indirect recursive binding

--

-- > x := x args1      x := y args1

-- >                   y := x args2

--

-- where @args1, args2@ are non-empty lists of arguments, /cannot/ be relevant:

-- if they were, that would imply that there is some type constructor (regular

-- datatype or type family) which can be applied to an arbitrary number of

-- arguments. Such datatypes or type families cannot be defined in Haskell.

-- We therefore take no special care in handling recursive bindings, other than

-- to note (as we did above) that the process must terminate.

process :: Classified -> TyConSubst
process :: Classified -> TyConSubst
process Classified{[(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
[(TcTyVar, (TyCon, [Type]), [Coercion])]
[(TcTyVar, TcTyVar, [Coercion])]
classifiedProductive :: Classified -> [(TcTyVar, (TyCon, [Type]), [Coercion])]
classifiedExtendEquivClass :: Classified -> [(TcTyVar, TcTyVar, [Coercion])]
classifiedReconsider :: Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
classifiedProductive :: [(TcTyVar, (TyCon, [Type]), [Coercion])]
classifiedExtendEquivClass :: [(TcTyVar, TcTyVar, [Coercion])]
classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
..} =
    TyConSubst
-> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])] -> TyConSubst
go TyConSubst
initSubst [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
classifiedReconsider
  where
    initSubst :: TyConSubst
    initSubst :: TyConSubst
initSubst =
          [(TcTyVar, (TyCon, [Type]), [Coercion])]
-> TyConSubst -> TyConSubst
tyConSubstExtend [(TcTyVar, (TyCon, [Type]), [Coercion])]
classifiedProductive
        (TyConSubst -> TyConSubst) -> TyConSubst -> TyConSubst
forall a b. (a -> b) -> a -> b
$ UniqFM TcTyVar (TcTyVar, [Coercion]) -> TyConSubst
tyConSubstEmpty ([(TcTyVar, TcTyVar, [Coercion])]
-> UniqFM TcTyVar (TcTyVar, [Coercion])
forall a l.
(Uniquable a, Monoid l) =>
[(a, a, l)] -> UniqFM a (a, l)
constructEquivClasses [(TcTyVar, TcTyVar, [Coercion])]
classifiedExtendEquivClass)

    go :: TyConSubst
       -> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
       -> TyConSubst
    go :: TyConSubst
-> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])] -> TyConSubst
go TyConSubst
acc [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
rs =
        let ([(TcTyVar, (TyCon, [Type]), [Coercion])]
prod, [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
rest) = ((TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])
 -> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion])))
-> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
-> ([(TcTyVar, (TyCon, [Type]), [Coercion])],
    [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])])
forall a b. (a -> Maybe (NonEmpty b)) -> [a] -> ([b], [a])
tryApply (TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])
-> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion]))
makeProductive [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
rs in
        if [(TcTyVar, (TyCon, [Type]), [Coercion])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TcTyVar, (TyCon, [Type]), [Coercion])]
prod
          then TyConSubst
acc -- No other equations can be made productive

          else TyConSubst
-> [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])] -> TyConSubst
go ([(TcTyVar, (TyCon, [Type]), [Coercion])]
-> TyConSubst -> TyConSubst
tyConSubstExtend [(TcTyVar, (TyCon, [Type]), [Coercion])]
prod TyConSubst
acc) [(TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])]
rest
      where
        makeProductive ::
             (TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])
          -> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion]))
        makeProductive :: (TcTyVar, (TcTyVar, NonEmpty Type), [Coercion])
-> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion]))
makeProductive (TcTyVar
var, (TcTyVar
var', NonEmpty Type
args), [Coercion]
deps) = do
          NonEmpty (TyCon, [Type], [Coercion])
tcApp <- TcTyVar
-> TyConSubst -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstLookup TcTyVar
var' TyConSubst
acc
          NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion])
-> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion]))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion])
 -> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion])))
-> NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion])
-> Maybe (NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion]))
forall a b. (a -> b) -> a -> b
$ ((TyCon, [Type], [Coercion])
 -> (TcTyVar, (TyCon, [Type]), [Coercion]))
-> NonEmpty (TyCon, [Type], [Coercion])
-> NonEmpty (TcTyVar, (TyCon, [Type]), [Coercion])
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyCon, [Type], [Coercion])
-> (TcTyVar, (TyCon, [Type]), [Coercion])
aux NonEmpty (TyCon, [Type], [Coercion])
tcApp
          where
            aux :: (TyCon, [Type], [Coercion]) -> (TcTyVar, (TyCon, [Type]), [Coercion])
            aux :: (TyCon, [Type], [Coercion])
-> (TcTyVar, (TyCon, [Type]), [Coercion])
aux (TyCon
tyCon, [Type]
args', [Coercion]
deps') =
              (TcTyVar
var, (TyCon
tyCon, [Type]
args' [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ NonEmpty Type -> [Type]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty Type
args), [Coercion]
deps [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion]
deps')

-- | Construct a 'TyConSubst' from a collection of Given constraints.

mkTyConSubst :: [Ct] -> TyConSubst
mkTyConSubst :: [Ct] -> TyConSubst
mkTyConSubst = Classified -> TyConSubst
process (Classified -> TyConSubst)
-> ([Ct] -> Classified) -> [Ct] -> TyConSubst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ct] -> Classified
classify

{-------------------------------------------------------------------------------
  Using
-------------------------------------------------------------------------------}

-- | Like 'splitTyConApp_maybe', but taking Given constraints into account.

--

-- Alongside the @TyCon@ and its arguments, also returns a list of coercions

-- that embody the Givens that we depended on.

--

-- Looks through type synonyms, just like 'splitTyConApp_maybe' does.

splitTyConApp_upTo :: TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
splitTyConApp_upTo :: TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
splitTyConApp_upTo TyConSubst
subst Type
typ = [Maybe (NonEmpty (TyCon, [Type], [Coercion]))]
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum [
      -- Direct match

      do (TyCon
tyCon, [Type]
inner) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
fn
         NonEmpty (TyCon, [Type], [Coercion])
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TyCon
tyCon, [Type]
inner [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args, []) (TyCon, [Type], [Coercion])
-> [(TyCon, [Type], [Coercion])]
-> NonEmpty (TyCon, [Type], [Coercion])
forall a. a -> [a] -> NonEmpty a
:| [])

      -- Indirect match

    , do TcTyVar
var <- Type -> Maybe TcTyVar
getTyVar_maybe Type
fn
         NonEmpty (TyCon, [Type], [Coercion])
tcApps <- TcTyVar
-> TyConSubst -> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstLookup TcTyVar
var TyConSubst
subst
         NonEmpty (TyCon, [Type], [Coercion])
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty (TyCon, [Type], [Coercion])
 -> Maybe (NonEmpty (TyCon, [Type], [Coercion])))
-> NonEmpty (TyCon, [Type], [Coercion])
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall a b. (a -> b) -> a -> b
$
           ((TyCon, [Type], [Coercion]) -> (TyCon, [Type], [Coercion]))
-> NonEmpty (TyCon, [Type], [Coercion])
-> NonEmpty (TyCon, [Type], [Coercion])
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (TyCon
tc, [Type]
inner, [Coercion]
deps) -> (TyCon
tc, [Type]
inner [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args, [Coercion]
deps)) NonEmpty (TyCon, [Type], [Coercion])
tcApps
    ]
  where
    (Type
fn, [Type]
args) = Type -> (Type, [Type])
splitAppTys Type
typ

{-------------------------------------------------------------------------------
  Outputable
-------------------------------------------------------------------------------}

instance Outputable TyConSubst where
  ppr :: TyConSubst -> SDoc
ppr TyConSubst{UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: TyConSubst -> UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: TyConSubst -> UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: UniqFM TcTyVar (TcTyVar, [Coercion])
..} = SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
parens (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
          String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TyConSubst"
      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion])) -> SDoc
forall a. Outputable a => a -> SDoc
ppr UniqFM TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap
      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> UniqFM TcTyVar (TcTyVar, [Coercion]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr UniqFM TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon

{-------------------------------------------------------------------------------
  Canonical equalities
-------------------------------------------------------------------------------}

isCanonicalVarEq :: Ct -> Maybe (TcTyVar, Type, EqRel)
isCanonicalVarEq :: Ct -> Maybe (TcTyVar, Type, EqRel)
isCanonicalVarEq = \case
#if __GLASGOW_HASKELL__ < 902
    CTyEqCan { cc_tyvar, cc_rhs, cc_eq_rel } ->
      Just (cc_tyvar, cc_rhs, cc_eq_rel)
    CFunEqCan { cc_fsk, cc_fun, cc_tyargs } ->
      Just (cc_fsk, mkTyConApp cc_fun cc_tyargs, NomEq)
#elif __GLASGOW_HASKELL__ < 907
    CEqCan { cc_lhs, cc_rhs, cc_eq_rel }
      | TyVarLHS var <- cc_lhs
      -> Just (var, cc_rhs, cc_eq_rel)
      | TyFamLHS tyCon args <- cc_lhs
      , Just var            <- getTyVar_maybe cc_rhs
      -> Just (var, mkTyConApp tyCon args, NomEq)
#else
    CEqCan EqCt
eqCt
      | TyVarLHS TcTyVar
var <- CanEqLHS
lhs
      -> (TcTyVar, Type, EqRel) -> Maybe (TcTyVar, Type, EqRel)
forall a. a -> Maybe a
Just (TcTyVar
var, Type
rhs, EqRel
rel)
      | TyFamLHS TyCon
tyCon [Type]
args <- CanEqLHS
lhs
      , Just TcTyVar
var            <- Type -> Maybe TcTyVar
getTyVar_maybe Type
rhs
      -> (TcTyVar, Type, EqRel) -> Maybe (TcTyVar, Type, EqRel)
forall a. a -> Maybe a
Just (TcTyVar
var, TyCon -> [Type] -> Type
mkTyConApp TyCon
tyCon [Type]
args, EqRel
rel)
      where
        lhs :: CanEqLHS
lhs = EqCt -> CanEqLHS
eq_lhs EqCt
eqCt
        rhs :: Type
rhs = EqCt -> Type
eq_rhs EqCt
eqCt
        rel :: EqRel
rel = EqCt -> EqRel
eq_eq_rel EqCt
eqCt
#endif
    -- Deal with CNonCanonical, which are produced by ghc-tcplugin-api

    -- in GHC 9.0 and below due to 'unflattenCts'.

    ct :: Ct
ct@(CNonCanonical {})
      | EqPred EqRel
rel Type
lhs Type
rhs <- Type -> Pred
classifyPredType (Ct -> Type
ctPred Ct
ct)
      -> if | Just TcTyVar
tv <- Type -> Maybe TcTyVar
getTyVar_maybe Type
lhs
            -> (TcTyVar, Type, EqRel) -> Maybe (TcTyVar, Type, EqRel)
forall a. a -> Maybe a
Just (TcTyVar
tv, Type
rhs, EqRel
rel)
            | Just TcTyVar
tv <- Type -> Maybe TcTyVar
getTyVar_maybe Type
rhs
            -> (TcTyVar, Type, EqRel) -> Maybe (TcTyVar, Type, EqRel)
forall a. a -> Maybe a
Just (TcTyVar
tv, Type
lhs, EqRel
rel)
            | Bool
otherwise
            -> Maybe (TcTyVar, Type, EqRel)
forall a. Maybe a
Nothing
    Ct
_ -> Maybe (TcTyVar, Type, EqRel)
forall a. Maybe a
Nothing

{-------------------------------------------------------------------------------
  Internal auxiliary
-------------------------------------------------------------------------------}

-- | Attempt to apply a non-deterministic function to a list of values

--

-- Returns the successful results as well as the inputs on which the function

-- failed.

tryApply :: forall a b. (a -> Maybe (NonEmpty b)) -> [a] -> ([b], [a])
tryApply :: forall a b. (a -> Maybe (NonEmpty b)) -> [a] -> ([b], [a])
tryApply a -> Maybe (NonEmpty b)
f = ([NonEmpty b] -> [b]) -> ([NonEmpty b], [a]) -> ([b], [a])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([[b]] -> [b]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[b]] -> [b]) -> ([NonEmpty b] -> [[b]]) -> [NonEmpty b] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty b -> [b]) -> [NonEmpty b] -> [[b]]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty b -> [b]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList) (([NonEmpty b], [a]) -> ([b], [a]))
-> ([a] -> ([NonEmpty b], [a])) -> [a] -> ([b], [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Either (NonEmpty b) a] -> ([NonEmpty b], [a])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (NonEmpty b) a] -> ([NonEmpty b], [a]))
-> ([a] -> [Either (NonEmpty b) a]) -> [a] -> ([NonEmpty b], [a])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Either (NonEmpty b) a) -> [a] -> [Either (NonEmpty b) a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Either (NonEmpty b) a
f'
  where
    f' :: a -> Either (NonEmpty b) a
    f' :: a -> Either (NonEmpty b) a
f' a
a = Either (NonEmpty b) a
-> (NonEmpty b -> Either (NonEmpty b) a)
-> Maybe (NonEmpty b)
-> Either (NonEmpty b) a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> Either (NonEmpty b) a
forall a b. b -> Either a b
Right a
a) NonEmpty b -> Either (NonEmpty b) a
forall a b. a -> Either a b
Left (Maybe (NonEmpty b) -> Either (NonEmpty b) a)
-> Maybe (NonEmpty b) -> Either (NonEmpty b) a
forall a b. (a -> b) -> a -> b
$ a -> Maybe (NonEmpty b)
f a
a

{-------------------------------------------------------------------------------
  Equivalence classes
-------------------------------------------------------------------------------}

-- | Given a set of labelled equivalent pairs, map every value to a canonical

-- value in the same equivalence class, with the shortest path (as a list of

-- labels) connecting the value to the canonical value.

--

-- Example with two equivalence classes:

--

-- >>> constructEquivClasses [(1, 2, ["12"]), (4, 5, ["45"]), (2, 3, ["23"])]

-- fromList [(1,(1,[])),(2,(1,["12"])),(3,(1,["23","12"])),(4,(4,[])),(5,(4,["45"]))]

--

-- Adding one element that connects both equivalence classes:

--

-- >>> constructEquivClasses [(1, 2, ["12"]), (4, 5, ["45"]), (2, 3, ["23"]), (3, 4, ["34"])]

-- fromList [(1,(1,[])),(2,(1,["12"])),(3,(1,["23","12"])),(4,(1,["34","23","12"])),(5,(1,["45","34","23","12"]))]

constructEquivClasses :: forall a l. (Uniquable a, Monoid l) => [(a, a, l)] -> UniqFM a (a, l)
constructEquivClasses :: forall a l.
(Uniquable a, Monoid l) =>
[(a, a, l)] -> UniqFM a (a, l)
constructEquivClasses [(a, a, l)]
equivs = UniqFM a (a, l)
canonicals
  where
    neighbours :: UniqFM a (UniqFM a l)
    neighbours :: UniqFM a (UniqFM a l)
neighbours = [(a, a, l)] -> UniqFM a (UniqFM a l)
forall a l. Uniquable a => [(a, a, l)] -> UniqFM a (UniqFM a l)
neighboursMap [(a, a, l)]
equivs

    allValues :: UniqSet a
    allValues :: UniqSet a
allValues = [a] -> UniqSet a
forall a. Uniquable a => [a] -> UniqSet a
UniqSet.mkUniqSet ([a] -> UniqSet a) -> [a] -> UniqSet a
forall a b. (a -> b) -> a -> b
$ [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [a
x,a
y] | (a
x,a
y,l
_) <- [(a, a, l)]
equivs ]

    canonicals :: UniqFM a (a, l)
    canonicals :: UniqFM a (a, l)
canonicals = UniqFM a (a, l) -> UniqSet a -> UniqFM a (a, l)
go UniqFM a (a, l)
forall key elt. UniqFM key elt
UFM.emptyUFM UniqSet a
allValues
      where
        go :: UniqFM a (a, l) -> UniqSet a -> UniqFM a (a, l)
        go :: UniqFM a (a, l) -> UniqSet a -> UniqFM a (a, l)
go UniqFM a (a, l)
acc UniqSet a
vs =
          case UniqSet a -> Maybe (a, UniqSet a)
forall a. UniqSet a -> Maybe (a, UniqSet a)
minViewUniqSet UniqSet a
vs of
            Maybe (a, UniqSet a)
Nothing -> UniqFM a (a, l)
acc
            Just (a
v, UniqSet a
vs') ->
              let
                !comp :: UniqFM a l
comp = UniqFM a l -> Seq Unique -> UniqFM a l
doComp
                          ( a -> l -> UniqFM a l
forall key elt. Uniquable key => key -> elt -> UniqFM key elt
UFM.unitUFM a
v l
forall a. Monoid a => a
mempty )
                          ( Unique -> Seq Unique
forall a. a -> Seq a
Seq.singleton (Unique -> Seq Unique) -> Unique -> Seq Unique
forall a b. (a -> b) -> a -> b
$ a -> Unique
forall a. Uniquable a => a -> Unique
getUnique a
v )
              in
                UniqFM a (a, l) -> UniqSet a -> UniqFM a (a, l)
go
                  ( UniqFM a (a, l) -> UniqFM a (a, l) -> UniqFM a (a, l)
forall key elt. UniqFM key elt -> UniqFM key elt -> UniqFM key elt
UFM.plusUFM UniqFM a (a, l)
acc ( ( a
v , ) (l -> (a, l)) -> UniqFM a l -> UniqFM a (a, l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UniqFM a l
comp ) )
                  ( UniqSet a
vs' UniqSet a -> UniqFM a l -> UniqSet a
forall key b. UniqSet key -> UniqFM key b -> UniqSet key
`UniqSet.uniqSetMinusUFM` UniqFM a l
comp )

        doComp :: UniqFM a l -> Seq Unique -> UniqFM a l
        doComp :: UniqFM a l -> Seq Unique -> UniqFM a l
doComp !UniqFM a l
ds Seq Unique
Seq.Empty = UniqFM a l
ds
        doComp  UniqFM a l
ds (Unique
v Seq.:<| Seq Unique
vs) =
          let
            -- unvisited neighbours

            !us :: UniqFM a l
us = ( Maybe (UniqFM a l) -> UniqFM a l
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (UniqFM a l) -> UniqFM a l)
-> Maybe (UniqFM a l) -> UniqFM a l
forall a b. (a -> b) -> a -> b
$ UniqFM a (UniqFM a l) -> Unique -> Maybe (UniqFM a l)
forall key elt. UniqFM key elt -> Unique -> Maybe elt
UFM.lookupUFM_Directly UniqFM a (UniqFM a l)
neighbours Unique
v ) UniqFM a l -> UniqFM a l -> UniqFM a l
forall key elt1 elt2.
UniqFM key elt1 -> UniqFM key elt2 -> UniqFM key elt1
`UFM.minusUFM` UniqFM a l
ds
            !d :: l
d = Maybe l -> l
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe l -> l) -> Maybe l -> l
forall a b. (a -> b) -> a -> b
$ UniqFM a l -> Unique -> Maybe l
forall key elt. UniqFM key elt -> Unique -> Maybe elt
UFM.lookupUFM_Directly UniqFM a l
ds Unique
v

            !ds' :: UniqFM a l
ds' = UniqFM a l -> UniqFM a l -> UniqFM a l
forall key elt. UniqFM key elt -> UniqFM key elt -> UniqFM key elt
UFM.plusUFM UniqFM a l
ds ( (l -> l) -> UniqFM a l -> UniqFM a l
forall elt1 elt2 key.
(elt1 -> elt2) -> UniqFM key elt1 -> UniqFM key elt2
UFM.mapUFM (l -> l -> l
forall a. Semigroup a => a -> a -> a
<> l
d) UniqFM a l
us )
            !vs' :: Seq Unique
vs' = Seq Unique
vs Seq Unique -> Seq Unique -> Seq Unique
forall a. Seq a -> Seq a -> Seq a
Seq.>< [Unique] -> Seq Unique
forall a. [a] -> Seq a
Seq.fromList ( UniqFM a l -> [Unique]
forall key elt. UniqFM key elt -> [Unique]
UFM.nonDetKeysUFM UniqFM a l
us )
          in
            UniqFM a l -> Seq Unique -> UniqFM a l
doComp UniqFM a l
ds' Seq Unique
vs'

minViewUniqSet :: forall a. UniqSet a -> Maybe (a, UniqSet a)
minViewUniqSet :: forall a. UniqSet a -> Maybe (a, UniqSet a)
minViewUniqSet UniqSet a
s =
  let m :: Word64Map a
m = UniqFM a a -> Word64Map a
forall key elt. UniqFM key elt -> Word64Map elt
UFM.ufmToIntMap (UniqFM a a -> Word64Map a) -> UniqFM a a -> Word64Map a
forall a b. (a -> b) -> a -> b
$ UniqSet a -> UniqFM a a
forall a. UniqSet a -> UniqFM a a
UniqSet.getUniqSet UniqSet a
s
  in (Word64Map a -> UniqSet a) -> (a, Word64Map a) -> (a, UniqSet a)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
        ( UniqFM a a -> UniqSet a
forall a. UniqFM a a -> UniqSet a
UniqSet.unsafeUFMToUniqSet
            (UniqFM a a -> UniqSet a)
-> (Word64Map a -> UniqFM a a) -> Word64Map a -> UniqSet a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
#if MIN_VERSION_ghc(8,11,0)
          Word64Map a -> UniqFM a a
forall elt key. Word64Map elt -> UniqFM key elt
UFM.unsafeIntMapToUFM
#else
          ( unsafeCoerce :: IntMap.IntMap a -> UniqFM a a )
#endif
        ) ((a, Word64Map a) -> (a, UniqSet a))
-> Maybe (a, Word64Map a) -> Maybe (a, UniqSet a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
#if HAS_WORD64MAP
      Word64Map a -> Maybe (a, Word64Map a)
forall a. Word64Map a -> Maybe (a, Word64Map a)
Word64Map.minView
#else
      IntMap.minView
#endif
        Word64Map a
m

neighboursMap :: forall a l. Uniquable a => [(a, a, l)] -> UniqFM a (UniqFM a l)
neighboursMap :: forall a l. Uniquable a => [(a, a, l)] -> UniqFM a (UniqFM a l)
neighboursMap [(a, a, l)]
edges = ((a, a, l) -> UniqFM a (UniqFM a l) -> UniqFM a (UniqFM a l))
-> UniqFM a (UniqFM a l) -> [(a, a, l)] -> UniqFM a (UniqFM a l)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a, a, l) -> UniqFM a (UniqFM a l) -> UniqFM a (UniqFM a l)
addEdge UniqFM a (UniqFM a l)
forall key elt. UniqFM key elt
UFM.emptyUFM [(a, a, l)]
edges
  where
    addEdge :: (a, a, l) -> UniqFM a (UniqFM a l) -> UniqFM a (UniqFM a l)
    addEdge :: (a, a, l) -> UniqFM a (UniqFM a l) -> UniqFM a (UniqFM a l)
addEdge (a
u, a
v, l
l) UniqFM a (UniqFM a l)
m
      = (UniqFM a l -> UniqFM a l -> UniqFM a l)
-> UniqFM a (UniqFM a l)
-> a
-> UniqFM a l
-> UniqFM a (UniqFM a l)
forall key elt.
Uniquable key =>
(elt -> elt -> elt)
-> UniqFM key elt -> key -> elt -> UniqFM key elt
UFM.addToUFM_C UniqFM a l -> UniqFM a l -> UniqFM a l
forall key elt. UniqFM key elt -> UniqFM key elt -> UniqFM key elt
UFM.plusUFM
          ((UniqFM a l -> UniqFM a l -> UniqFM a l)
-> UniqFM a (UniqFM a l)
-> a
-> UniqFM a l
-> UniqFM a (UniqFM a l)
forall key elt.
Uniquable key =>
(elt -> elt -> elt)
-> UniqFM key elt -> key -> elt -> UniqFM key elt
UFM.addToUFM_C UniqFM a l -> UniqFM a l -> UniqFM a l
forall key elt. UniqFM key elt -> UniqFM key elt -> UniqFM key elt
UFM.plusUFM UniqFM a (UniqFM a l)
m a
v (a -> l -> UniqFM a l
forall key elt. Uniquable key => key -> elt -> UniqFM key elt
UFM.unitUFM a
u l
l))
          a
u (a -> l -> UniqFM a l
forall key elt. Uniquable key => key -> elt -> UniqFM key elt
UFM.unitUFM a
v l
l)

canonicalize :: (Uniquable a, Monoid l) => UniqFM a (a, l) -> a -> (a, l)
canonicalize :: forall a l.
(Uniquable a, Monoid l) =>
UniqFM a (a, l) -> a -> (a, l)
canonicalize UniqFM a (a, l)
canon a
x = UniqFM a (a, l) -> (a, l) -> a -> (a, l)
forall key elt.
Uniquable key =>
UniqFM key elt -> elt -> key -> elt
UFM.lookupWithDefaultUFM UniqFM a (a, l)
canon (a
x, l
forall a. Monoid a => a
mempty) a
x