{-# LANGUAGE CPP #-}

{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# 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

-- base

import Data.Bifunctor
import Data.Either
  ( partitionEithers )
import Data.Foldable
  ( toList, asum )
import Data.List.NonEmpty
  ( NonEmpty(..) )

-- containers

import Data.Graph
  ( Graph, Vertex )
import qualified Data.Graph as Graph
import Data.Map
  ( Map )
import qualified Data.Map as Map
import Data.Set
  ( Set )
import qualified Data.Set as Set

-- ghc

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 -> Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type]))
    , TyConSubst -> Map TcTyVar TcTyVar
tyConSubstCanon :: Map TcTyVar TcTyVar
    }
-- 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 canononical 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 :: Map TcTyVar TcTyVar -> TyConSubst
tyConSubstEmpty :: Map TcTyVar TcTyVar -> TyConSubst
tyConSubstEmpty Map TcTyVar TcTyVar
canon = TyConSubst {
      tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstMap   = Map TcTyVar (NonEmpty (TyCon, [Type]))
forall k a. Map k a
Map.empty
    , tyConSubstCanon :: Map TcTyVar TcTyVar
tyConSubstCanon = Map TcTyVar TcTyVar
canon
    }

-- | Lookup a variable in the substitution

tyConSubstLookup :: TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type]))
tyConSubstLookup :: TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type]))
tyConSubstLookup TcTyVar
var TyConSubst{Map TcTyVar (NonEmpty (TyCon, [Type]))
Map TcTyVar TcTyVar
tyConSubstMap :: TyConSubst -> Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstCanon :: TyConSubst -> Map TcTyVar TcTyVar
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstCanon :: Map TcTyVar TcTyVar
..} = TcTyVar
-> Map TcTyVar (NonEmpty (TyCon, [Type]))
-> Maybe (NonEmpty (TyCon, [Type]))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TcTyVar
var' Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstMap
  where
    var' :: TcTyVar
    var' :: TcTyVar
var' = Map TcTyVar TcTyVar -> TcTyVar -> TcTyVar
forall a. Ord a => Map a a -> a -> a
canonicalize Map TcTyVar TcTyVar
tyConSubstCanon TcTyVar
var

-- | Extend substitution with new bindings

tyConSubstExtend ::
     [(TcTyVar, (TyCon, [Type]))]
  -> TyConSubst -> TyConSubst
tyConSubstExtend :: [(TcTyVar, (TyCon, [Type]))] -> TyConSubst -> TyConSubst
tyConSubstExtend [(TcTyVar, (TyCon, [Type]))]
new subst :: TyConSubst
subst@TyConSubst{Map TcTyVar (NonEmpty (TyCon, [Type]))
Map TcTyVar TcTyVar
tyConSubstMap :: TyConSubst -> Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstCanon :: TyConSubst -> Map TcTyVar TcTyVar
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstCanon :: Map TcTyVar TcTyVar
..} = TyConSubst
subst {
      tyConSubstMap = Map.unionWith (<>)
                        (Map.fromList $ map (uncurry aux) new)
                        tyConSubstMap
    }
  where
    aux :: TcTyVar -> (TyCon, [Type]) -> (TcTyVar, NonEmpty (TyCon, [Type]))
    aux :: TcTyVar -> (TyCon, [Type]) -> (TcTyVar, NonEmpty (TyCon, [Type]))
aux TcTyVar
var (TyCon, [Type])
s = (Map TcTyVar TcTyVar -> TcTyVar -> TcTyVar
forall a. Ord a => Map a a -> a -> a
canonicalize Map TcTyVar TcTyVar
tyConSubstCanon TcTyVar
var, (TyCon, [Type])
s (TyCon, [Type]) -> [(TyCon, [Type])] -> NonEmpty (TyCon, [Type])
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]))]
classifiedProductive :: [(TcTyVar, (TyCon, [Type]))]

      -- | Extend equivalence class of variables

      --

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

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

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

      -- | 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))]
classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type))]
    }

instance Semigroup Classified where
  Classified
c1 <> :: Classified -> Classified -> Classified
<> Classified
c2 = Classified {
        classifiedProductive :: [(TcTyVar, (TyCon, [Type]))]
classifiedProductive       = (Classified -> [(TcTyVar, (TyCon, [Type]))])
-> [(TcTyVar, (TyCon, [Type]))]
forall a. (Classified -> [a]) -> [a]
combine Classified -> [(TcTyVar, (TyCon, [Type]))]
classifiedProductive
      , classifiedExtendEquivClass :: [(TcTyVar, TcTyVar)]
classifiedExtendEquivClass = (Classified -> [(TcTyVar, TcTyVar)]) -> [(TcTyVar, TcTyVar)]
forall a. (Classified -> [a]) -> [a]
combine Classified -> [(TcTyVar, TcTyVar)]
classifiedExtendEquivClass
      , classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type))]
classifiedReconsider       = (Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type))])
-> [(TcTyVar, (TcTyVar, NonEmpty Type))]
forall a. (Classified -> [a]) -> [a]
combine Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type))]
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]))]
-> [(TcTyVar, TcTyVar)]
-> [(TcTyVar, (TcTyVar, NonEmpty Type))]
-> Classified
Classified [] [] []

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

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

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

-- | 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) =
        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]) -> Classified
productive TcTyVar
var (TyCon
tyCon, [Type]
inner [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args) 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 -> Classified
extendEquivClass TcTyVar
var TcTyVar
var' 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) -> Classified
reconsider TcTyVar
var (TcTyVar
var', Type
x Type -> [Type] -> NonEmpty Type
forall a. a -> [a] -> NonEmpty a
:| [Type]
xs) 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 acocunt, 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))]
[(TcTyVar, (TyCon, [Type]))]
[(TcTyVar, TcTyVar)]
classifiedProductive :: Classified -> [(TcTyVar, (TyCon, [Type]))]
classifiedExtendEquivClass :: Classified -> [(TcTyVar, TcTyVar)]
classifiedReconsider :: Classified -> [(TcTyVar, (TcTyVar, NonEmpty Type))]
classifiedProductive :: [(TcTyVar, (TyCon, [Type]))]
classifiedExtendEquivClass :: [(TcTyVar, TcTyVar)]
classifiedReconsider :: [(TcTyVar, (TcTyVar, NonEmpty Type))]
..} =
    TyConSubst -> [(TcTyVar, (TcTyVar, NonEmpty Type))] -> TyConSubst
go TyConSubst
initSubst [(TcTyVar, (TcTyVar, NonEmpty Type))]
classifiedReconsider
  where
    initSubst :: TyConSubst
    initSubst :: TyConSubst
initSubst =
          [(TcTyVar, (TyCon, [Type]))] -> TyConSubst -> TyConSubst
tyConSubstExtend [(TcTyVar, (TyCon, [Type]))]
classifiedProductive
        (TyConSubst -> TyConSubst) -> TyConSubst -> TyConSubst
forall a b. (a -> b) -> a -> b
$ Map TcTyVar TcTyVar -> TyConSubst
tyConSubstEmpty ([(TcTyVar, TcTyVar)] -> Map TcTyVar TcTyVar
forall a. Ord a => [(a, a)] -> Map a a
constructEquivClasses [(TcTyVar, TcTyVar)]
classifiedExtendEquivClass)

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

          else TyConSubst -> [(TcTyVar, (TcTyVar, NonEmpty Type))] -> TyConSubst
go ([(TcTyVar, (TyCon, [Type]))] -> TyConSubst -> TyConSubst
tyConSubstExtend [(TcTyVar, (TyCon, [Type]))]
prod TyConSubst
acc) [(TcTyVar, (TcTyVar, NonEmpty Type))]
rest
      where
        makeProductive ::
             (TcTyVar, (TcTyVar, NonEmpty Type))
          -> Maybe (NonEmpty (TcTyVar, (TyCon, [Type])))
        makeProductive :: (TcTyVar, (TcTyVar, NonEmpty Type))
-> Maybe (NonEmpty (TcTyVar, (TyCon, [Type])))
makeProductive (TcTyVar
var, (TcTyVar
var', NonEmpty Type
args)) =
            (NonEmpty (TyCon, [Type]) -> NonEmpty (TcTyVar, (TyCon, [Type])))
-> Maybe (NonEmpty (TyCon, [Type]))
-> Maybe (NonEmpty (TcTyVar, (TyCon, [Type])))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((TyCon, [Type]) -> (TcTyVar, (TyCon, [Type])))
-> NonEmpty (TyCon, [Type]) -> NonEmpty (TcTyVar, (TyCon, [Type]))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyCon -> [Type] -> (TcTyVar, (TyCon, [Type])))
-> (TyCon, [Type]) -> (TcTyVar, (TyCon, [Type]))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyCon -> [Type] -> (TcTyVar, (TyCon, [Type]))
aux)) (TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type]))
tyConSubstLookup TcTyVar
var' TyConSubst
acc)
          where
            aux :: TyCon -> [Type] -> (TcTyVar, (TyCon, [Type]))
            aux :: TyCon -> [Type] -> (TcTyVar, (TyCon, [Type]))
aux TyCon
tyCon [Type]
args' = (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)))

-- | 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.

--

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

splitTyConApp_upTo :: TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type]))
splitTyConApp_upTo :: TyConSubst -> Type -> Maybe (NonEmpty (TyCon, [Type]))
splitTyConApp_upTo TyConSubst
subst Type
typ = [Maybe (NonEmpty (TyCon, [Type]))]
-> Maybe (NonEmpty (TyCon, [Type]))
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]) -> Maybe (NonEmpty (TyCon, [Type]))
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]) -> [(TyCon, [Type])] -> NonEmpty (TyCon, [Type])
forall a. a -> [a] -> NonEmpty a
:| [])

      -- Indirect match

    , do TcTyVar
var <- Type -> Maybe TcTyVar
getTyVar_maybe Type
fn
         (NonEmpty (TyCon, [Type]) -> NonEmpty (TyCon, [Type]))
-> Maybe (NonEmpty (TyCon, [Type]))
-> Maybe (NonEmpty (TyCon, [Type]))
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((TyCon, [Type]) -> (TyCon, [Type]))
-> NonEmpty (TyCon, [Type]) -> NonEmpty (TyCon, [Type])
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Type] -> [Type]) -> (TyCon, [Type]) -> (TyCon, [Type])
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 ([Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
args))) (Maybe (NonEmpty (TyCon, [Type]))
 -> Maybe (NonEmpty (TyCon, [Type])))
-> Maybe (NonEmpty (TyCon, [Type]))
-> Maybe (NonEmpty (TyCon, [Type]))
forall a b. (a -> b) -> a -> b
$ TcTyVar -> TyConSubst -> Maybe (NonEmpty (TyCon, [Type]))
tyConSubstLookup TcTyVar
var TyConSubst
subst
    ]
  where
    (Type
fn, [Type]
args) = Type -> (Type, [Type])
splitAppTys Type
typ

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

instance Outputable TyConSubst where
  ppr :: TyConSubst -> SDoc
ppr TyConSubst{Map TcTyVar (NonEmpty (TyCon, [Type]))
Map TcTyVar TcTyVar
tyConSubstMap :: TyConSubst -> Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstCanon :: TyConSubst -> Map TcTyVar TcTyVar
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstCanon :: Map TcTyVar TcTyVar
..} = 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
<+> Map TcTyVar (NonEmpty (TyCon, [Type])) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Map TcTyVar (NonEmpty (TyCon, [Type]))
tyConSubstMap
      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Map TcTyVar TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr Map TcTyVar TcTyVar
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)
    _otherwise    -> Nothing
#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)
    _otherwise
      -> Nothing
#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
    Ct
_otherwise
      -> Maybe (TcTyVar, Type, EqRel)
forall a. Maybe a
Nothing
#endif

{-------------------------------------------------------------------------------
  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 equivalent pairs, map every value to canonical value

--

-- Example with two classes:

--

-- >>> constructEquivClasses [(1, 2), (4, 5), (2, 3)]

-- fromList [(1,1),(2,1),(3,1),(4,4),(5,4)]

--

-- Adding one element that connects both classes:

--

-- >>> constructEquivClasses [(1, 2), (4, 5), (2, 3), (3, 4)]

-- fromList [(1,1),(2,1),(3,1),(4,1),(5,1)]

constructEquivClasses :: forall a. Ord a => [(a, a)] -> Map a a
constructEquivClasses :: forall a. Ord a => [(a, a)] -> Map a a
constructEquivClasses [(a, a)]
equivs =
     [Map a a] -> Map a a
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ([Map a a] -> Map a a) -> [Map a a] -> Map a a
forall a b. (a -> b) -> a -> b
$ (Tree Vertex -> Map a a) -> [Tree Vertex] -> [Map a a]
forall a b. (a -> b) -> [a] -> [b]
map ([a] -> Map a a
pickCanonical ([a] -> Map a a) -> (Tree Vertex -> [a]) -> Tree Vertex -> Map a a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Vertex -> a) -> [Vertex] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Vertex -> a
fromVertex ([Vertex] -> [a])
-> (Tree Vertex -> [Vertex]) -> Tree Vertex -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree Vertex -> [Vertex]
forall a. Tree a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList) ([Tree Vertex] -> [Map a a]) -> [Tree Vertex] -> [Map a a]
forall a b. (a -> b) -> a -> b
$
       Graph -> [Tree Vertex]
Graph.components Graph
graph
  where
    allValues :: Set a
    allValues :: Set a
allValues = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList ([a] -> Set a) -> [a] -> Set a
forall a b. (a -> b) -> a -> b
$ ((a, a) -> [a]) -> [(a, a)] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(a
x, a
y) -> [a
x, a
y]) [(a, a)]
equivs

    toVertex   :: a -> Vertex
    fromVertex :: Vertex -> a

    toVertex :: a -> Vertex
toVertex   a
a = Vertex -> a -> Map a Vertex -> Vertex
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Vertex
forall a. HasCallStack => String -> a
error String
"toVertex: impossible")   a
a (Map a Vertex -> Vertex) -> Map a Vertex -> Vertex
forall a b. (a -> b) -> a -> b
$
                     [(a, Vertex)] -> Map a Vertex
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(a, Vertex)] -> Map a Vertex) -> [(a, Vertex)] -> Map a Vertex
forall a b. (a -> b) -> a -> b
$ [a] -> [Vertex] -> [(a, Vertex)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
allValues) [Vertex
1..]
    fromVertex :: Vertex -> a
fromVertex Vertex
v = a -> Vertex -> Map Vertex a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> a
forall a. HasCallStack => String -> a
error String
"fromVertex: impossible") Vertex
v (Map Vertex a -> a) -> Map Vertex a -> a
forall a b. (a -> b) -> a -> b
$
                     [(Vertex, a)] -> Map Vertex a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Vertex, a)] -> Map Vertex a) -> [(Vertex, a)] -> Map Vertex a
forall a b. (a -> b) -> a -> b
$ [Vertex] -> [a] -> [(Vertex, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Vertex
1..] (Set a -> [a]
forall a. Set a -> [a]
Set.toList Set a
allValues)

    graph :: Graph
    graph :: Graph
graph = Bounds -> [Bounds] -> Graph
Graph.buildG (Vertex
1, Set a -> Vertex
forall a. Set a -> Vertex
Set.size Set a
allValues) ([Bounds] -> Graph) -> [Bounds] -> Graph
forall a b. (a -> b) -> a -> b
$
              ((a, a) -> Bounds) -> [(a, a)] -> [Bounds]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> Vertex) -> (a -> Vertex) -> (a, a) -> Bounds
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> Vertex
toVertex a -> Vertex
toVertex) [(a, a)]
equivs

    -- Given a previously established equivalence class, construct a mapping

    -- that maps each value to an (arbitrary) canonical value.

    pickCanonical :: [a] -> Map a a
    pickCanonical :: [a] -> Map a a
pickCanonical [a]
cls = [(a, a)] -> Map a a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(a, a)] -> Map a a) -> [(a, a)] -> Map a a
forall a b. (a -> b) -> a -> b
$ [a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
cls (a -> [a]
forall a. a -> [a]
repeat ([a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [a]
cls))

canonicalize :: Ord a => Map a a -> a -> a
canonicalize :: forall a. Ord a => Map a a -> a -> a
canonicalize Map a a
canon a
x = a -> a -> Map a a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault a
x a
x Map a a
canon