{-# 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(..) )

-- array

import qualified Data.Array as Array
  ( (!) )

-- 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], [Coercion]))
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
    , TyConSubst -> Map TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon :: Map 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 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, [Coercion]) -> TyConSubst
tyConSubstEmpty :: Map TcTyVar (TcTyVar, [Coercion]) -> TyConSubst
tyConSubstEmpty Map TcTyVar (TcTyVar, [Coercion])
canon = TyConSubst {
      tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap   = Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
forall k a. Map k a
Map.empty
    , tyConSubstCanon :: Map TcTyVar (TcTyVar, [Coercion])
tyConSubstCanon = Map 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{Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
Map TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: TyConSubst -> Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: TyConSubst -> Map TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: Map 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
<$> TcTyVar
-> Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
-> Maybe (NonEmpty (TyCon, [Type], [Coercion]))
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TcTyVar
var' Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap
  where
    var' :: TcTyVar
    deps' :: [Coercion]
    (TcTyVar
var', [Coercion]
deps') = Map TcTyVar (TcTyVar, [Coercion])
-> TcTyVar -> (TcTyVar, [Coercion])
forall a l. (Ord a, Monoid l) => Map a (a, l) -> a -> (a, l)
canonicalize Map 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{Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
Map TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: TyConSubst -> Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: TyConSubst -> Map TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: Map TcTyVar (TcTyVar, [Coercion])
..} = TyConSubst
subst {
      tyConSubstMap = Map.unionWith (<>)
                        (Map.fromList $ 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') = Map TcTyVar (TcTyVar, [Coercion])
-> TcTyVar -> (TcTyVar, [Coercion])
forall a l. (Ord a, Monoid l) => Map a (a, l) -> a -> (a, l)
canonicalize Map 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 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), [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
$ Map TcTyVar (TcTyVar, [Coercion]) -> TyConSubst
tyConSubstEmpty ([(TcTyVar, TcTyVar, [Coercion])]
-> Map TcTyVar (TcTyVar, [Coercion])
forall a l. (Ord a, Monoid l) => [(a, a, l)] -> Map 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{Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
Map TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: TyConSubst -> Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: TyConSubst -> Map TcTyVar (TcTyVar, [Coercion])
tyConSubstMap :: Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstCanon :: Map 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
<+> Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion])) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Map TcTyVar (NonEmpty (TyCon, [Type], [Coercion]))
tyConSubstMap
      SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Map TcTyVar (TcTyVar, [Coercion]) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Map 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)
    _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 labelled equivalent pairs, map every value to a canonical

-- value, with the shortest path (as a list of labels) connecting the value to

-- the canonical value.

--

-- Example with two classes:

--

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

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

--

-- Adding one element that connects both classes:

--

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

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

constructEquivClasses :: forall a l. (Ord a, Monoid l) => [(a, a, l)] -> Map a (a, l)
constructEquivClasses :: forall a l. (Ord a, Monoid l) => [(a, a, l)] -> Map a (a, l)
constructEquivClasses [(a, a, l)]
equivs
  = [Map a (a, l)] -> Map a (a, l)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions
  ([Map a (a, l)] -> Map a (a, l)) -> [Map a (a, l)] -> Map a (a, l)
forall a b. (a -> b) -> a -> b
$ (Tree Vertex -> Map a (a, l)) -> [Tree Vertex] -> [Map a (a, l)]
forall a b. (a -> b) -> [a] -> [b]
map ([a] -> Map a (a, l)
pickCanonical ([a] -> Map a (a, l))
-> (Tree Vertex -> [a]) -> Tree Vertex -> Map a (a, l)
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, l)])
-> [Tree Vertex] -> [Map a (a, l)]
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, l) -> [a]) -> [(a, a, l)] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(a
x, a
y, l
_) -> [a
x,a
y]) [(a, a, l)]
equivs

    edges :: Map (Set a) l
    edges :: Map (Set a) l
edges = [(Set a, l)] -> Map (Set a) l
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
x, a
y], l
lbl) | (a
x,a
y,l
lbl) <- [(a, a, l)]
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.elems 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.elems 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)
               [ (a -> Vertex
toVertex a
x, a -> Vertex
toVertex a
y) | (a
x, a
y, l
_) <- [(a, a, l)]
equivs]

    neighbours :: a -> [(a, l)]
    neighbours :: a -> [(a, l)]
neighbours a
v =
      [ ( a
u, Map (Set a) l
edges Map (Set a) l -> Set a -> l
forall k a. Ord k => Map k a -> k -> a
Map.! ( [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [ a
v, a
u ] ) )
      | a
u <- (Vertex -> a) -> [Vertex] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Vertex -> a
fromVertex ([Vertex] -> [a]) -> [Vertex] -> [a]
forall a b. (a -> b) -> a -> b
$ Graph
graph Graph -> Vertex -> [Vertex]
forall i e. Ix i => Array i e -> i -> e
Array.! ( a -> Vertex
toVertex a
v )
      ]

    pickCanonical :: [a] -> Map a (a, l)
    pickCanonical :: [a] -> Map a (a, l)
pickCanonical [a]
comp = ( a
root, ) (l -> (a, l)) -> Map a l -> Map a (a, l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map a l -> [a] -> Map a l
go ( a -> l -> Map a l
forall k a. k -> a -> Map k a
Map.singleton a
root l
forall a. Monoid a => a
mempty ) [ a
root ]
      where
        root :: a
root = [a] -> a
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [a]
comp

        go :: Map a l -> [a] -> Map a l
        go :: Map a l -> [a] -> Map a l
go Map a l
ds [] = Map a l
ds
        go Map a l
ds (a
v:[a]
vs) =
          let
            -- unvisited neighbours

            us :: [(a, l)]
us = ((a, l) -> Bool) -> [(a, l)] -> [(a, l)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (a
u, l
_) -> Bool -> Bool
not (a
u a -> Map a l -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map a l
ds) ) ([(a, l)] -> [(a, l)]) -> [(a, l)] -> [(a, l)]
forall a b. (a -> b) -> a -> b
$ a -> [(a, l)]
neighbours a
v

            d :: l
d = Map a l
ds Map a l -> a -> l
forall k a. Ord k => Map k a -> k -> a
Map.! a
v
            ds' :: Map a l
ds' = Map a l -> Map a l -> Map a l
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map a l
ds ([(a, l)] -> Map a l
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (a
u, l
l l -> l -> l
forall a. Semigroup a => a -> a -> a
<> l
d) | (a
u, l
l) <- [(a, l)]
us ])
          in
            Map a l -> [a] -> Map a l
go Map a l
ds' ([a]
vs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ ((a, l) -> a) -> [(a, l)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, l) -> a
forall a b. (a, b) -> a
fst [(a, l)]
us)

canonicalize :: (Ord a, Monoid l) => Map a (a, l) -> a -> (a, l)
canonicalize :: forall a l. (Ord a, Monoid l) => Map a (a, l) -> a -> (a, l)
canonicalize Map a (a, l)
canon a
x = (a, l) -> a -> Map a (a, l) -> (a, l)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (a
x, l
forall a. Monoid a => a
mempty) a
x Map a (a, l)
canon