{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE PolyKinds       #-}
{-# LANGUAGE TemplateHaskell #-}

-- | The internals of the normalizer.
module PlutusCore.Normalize.Internal (
  NormalizeTypeT,
  MonadNormalizeType,
  runNormalizeTypeT,
  withExtendedTypeVarEnv,
  normalizeTypeM,
  substNormalizeTypeM,
  normalizeTypesInM,
) where

import PlutusCore.Core.Plated (termSubterms, termSubtypes)
import PlutusCore.Core.Type (Normalized (..), Term, Type (..))
import PlutusCore.MkPlc (mkTyBuiltinOf)
import PlutusCore.Name.Unique (HasUnique, TypeUnique (TypeUnique), Unique (Unique))
import PlutusCore.Name.UniqueMap (UniqueMap, insertByName, lookupName)
import PlutusCore.Quote (MonadQuote)
import PlutusCore.Rename (Dupable, dupable, liftDupable)
import PlutusPrelude (Alternative, over, (<<$>>), (<<*>>))

import Control.Lens (makeLenses, transformMOf)
import Control.Monad (MonadPlus)
import Control.Monad.Reader (MonadReader (local), ReaderT (..), asks)
import Control.Monad.State (MonadState)
import Universe.Core (Esc, HasUniApply (matchUniApply), SomeTypeIn (SomeTypeIn))

{- Note [Global uniqueness in the normalizer]
WARNING: everything in this module works under the assumption that the global uniqueness condition
is satisfied. The invariant is not checked, enforced or automatically fulfilled. So you must ensure
that the global uniqueness condition is satisfied before calling ANY function from this module.

The invariant is preserved. In future we will enforce the invariant.
-}

{- | Mapping from variables to what they stand for (each row represents a substitution).
Needed for efficiency reasons, otherwise we could just use substitutions.
-}
type TypeVarEnv tyname uni ann = UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))

-- | The environments that type normalization runs in.
newtype NormalizeTypeEnv tyname uni ann = NormalizeTypeEnv
  { forall tyname (uni :: * -> *) ann.
NormalizeTypeEnv tyname uni ann -> TypeVarEnv tyname uni ann
_normalizeTypeEnvTypeVarEnv :: TypeVarEnv tyname uni ann
  }

makeLenses ''NormalizeTypeEnv

{- Note [NormalizeTypeT]
Type normalization requires 'Quote' (because we need to be able to generate fresh names), but we
do not put 'Quote' into 'NormalizeTypeT'. The reason for this is that it makes type signatures of
various runners much nicer and also more generic. For example, we have

    runNormalizeTypeT :: MonadQuote m => NormalizeTypeT m tyname uni ann a -> m a

If 'NormalizeTypeT' contained 'Quote', it would be

    runNormalizeTypeT :: NormalizeTypeT m tyname uni ann a -> QuoteT m a

which hardcodes 'QuoteT' to be the outermost transformer.

Type normalization can run in any @m@ (as long as it's a 'MonadQuote') as witnessed by
the following type signature:

    normalizeTypeM
        :: (HasUnique (tyname ann) TypeUnique, MonadQuote m)
        => Type tyname uni ann -> NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))

so it's natural to have runners that do not break this genericity.
-}

{- Note [Normalization API]
Normalization is split in two parts:

1. functions returning computations that perform reductions and run in defined in this module
   monad transformers (e.g. 'NormalizeTypeT')
2. runners of those computations

The reason for splitting the API is that this way the type-theoretic notion of normalization is
separated from implementation-specific details. (This used to be more important when we had
to deal with gas, and could maybe be changed now.)
-}

-- See Note [NormalizeTypeT].
-- | The monad transformer that type normalization runs in.
newtype NormalizeTypeT m tyname uni ann a = NormalizeTypeT
  { forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
unNormalizeTypeT :: ReaderT (NormalizeTypeEnv tyname uni ann) m a
  }
  deriving newtype
    ( (forall a b.
 (a -> b)
 -> NormalizeTypeT m tyname uni ann a
 -> NormalizeTypeT m tyname uni ann b)
-> (forall a b.
    a
    -> NormalizeTypeT m tyname uni ann b
    -> NormalizeTypeT m tyname uni ann a)
-> Functor (NormalizeTypeT m tyname uni ann)
forall a b.
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
$cfmap :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
fmap :: forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
$c<$ :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Functor m =>
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
<$ :: forall a b.
a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
Functor
    , Functor (NormalizeTypeT m tyname uni ann)
Functor (NormalizeTypeT m tyname uni ann) =>
(forall a. a -> NormalizeTypeT m tyname uni ann a)
-> (forall a b.
    NormalizeTypeT m tyname uni ann (a -> b)
    -> NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann b)
-> (forall a b c.
    (a -> b -> c)
    -> NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann b
    -> NormalizeTypeT m tyname uni ann c)
-> (forall a b.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann b
    -> NormalizeTypeT m tyname uni ann b)
-> (forall a b.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann b
    -> NormalizeTypeT m tyname uni ann a)
-> Applicative (NormalizeTypeT m tyname uni ann)
forall a. a -> NormalizeTypeT m tyname uni ann a
forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall a b.
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall a b c.
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Applicative m =>
Functor (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Applicative m =>
a -> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *) tyname (uni :: * -> *) ann a b c.
Applicative m =>
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
$cpure :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Applicative m =>
a -> NormalizeTypeT m tyname uni ann a
pure :: forall a. a -> NormalizeTypeT m tyname uni ann a
$c<*> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
<*> :: forall a b.
NormalizeTypeT m tyname uni ann (a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
$cliftA2 :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b c.
Applicative m =>
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
liftA2 :: forall a b c.
(a -> b -> c)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann c
$c*> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
*> :: forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
$c<* :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Applicative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
<* :: forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann a
Applicative
    , Applicative (NormalizeTypeT m tyname uni ann)
Applicative (NormalizeTypeT m tyname uni ann) =>
(forall a. NormalizeTypeT m tyname uni ann a)
-> (forall a.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann a)
-> (forall a.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann [a])
-> (forall a.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann [a])
-> Alternative (NormalizeTypeT m tyname uni ann)
forall a. NormalizeTypeT m tyname uni ann a
forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Alternative m =>
Applicative (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
$cempty :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
empty :: forall a. NormalizeTypeT m tyname uni ann a
$c<|> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
<|> :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
$csome :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
some :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
$cmany :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Alternative m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
many :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann [a]
Alternative
    , Applicative (NormalizeTypeT m tyname uni ann)
Applicative (NormalizeTypeT m tyname uni ann) =>
(forall a b.
 NormalizeTypeT m tyname uni ann a
 -> (a -> NormalizeTypeT m tyname uni ann b)
 -> NormalizeTypeT m tyname uni ann b)
-> (forall a b.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann b
    -> NormalizeTypeT m tyname uni ann b)
-> (forall a. a -> NormalizeTypeT m tyname uni ann a)
-> Monad (NormalizeTypeT m tyname uni ann)
forall a. a -> NormalizeTypeT m tyname uni ann a
forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall a b.
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (m :: * -> *) tyname (uni :: * -> *) ann.
Monad m =>
Applicative (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Monad m =>
a -> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
$c>>= :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
>>= :: forall a b.
NormalizeTypeT m tyname uni ann a
-> (a -> NormalizeTypeT m tyname uni ann b)
-> NormalizeTypeT m tyname uni ann b
$c>> :: forall (m :: * -> *) tyname (uni :: * -> *) ann a b.
Monad m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
>> :: forall a b.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
-> NormalizeTypeT m tyname uni ann b
$creturn :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
Monad m =>
a -> NormalizeTypeT m tyname uni ann a
return :: forall a. a -> NormalizeTypeT m tyname uni ann a
Monad
    , Monad (NormalizeTypeT m tyname uni ann)
Alternative (NormalizeTypeT m tyname uni ann)
(Alternative (NormalizeTypeT m tyname uni ann),
 Monad (NormalizeTypeT m tyname uni ann)) =>
(forall a. NormalizeTypeT m tyname uni ann a)
-> (forall a.
    NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann a
    -> NormalizeTypeT m tyname uni ann a)
-> MonadPlus (NormalizeTypeT m tyname uni ann)
forall a. NormalizeTypeT m tyname uni ann a
forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *).
(Alternative m, Monad m) =>
(forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
forall (m :: * -> *) tyname (uni :: * -> *) ann.
MonadPlus m =>
Monad (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann.
MonadPlus m =>
Alternative (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
$cmzero :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
mzero :: forall a. NormalizeTypeT m tyname uni ann a
$cmplus :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadPlus m =>
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
mplus :: forall a.
NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
MonadPlus
    , MonadReader (NormalizeTypeEnv tyname uni ann)
    , MonadState s
    , Monad (NormalizeTypeT m tyname uni ann)
Monad (NormalizeTypeT m tyname uni ann) =>
(forall a. Quote a -> NormalizeTypeT m tyname uni ann a)
-> MonadQuote (NormalizeTypeT m tyname uni ann)
forall a. Quote a -> NormalizeTypeT m tyname uni ann a
forall (m :: * -> *).
Monad m =>
(forall a. Quote a -> m a) -> MonadQuote m
forall (m :: * -> *) tyname (uni :: * -> *) ann.
MonadQuote m =>
Monad (NormalizeTypeT m tyname uni ann)
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadQuote m =>
Quote a -> NormalizeTypeT m tyname uni ann a
$cliftQuote :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
MonadQuote m =>
Quote a -> NormalizeTypeT m tyname uni ann a
liftQuote :: forall a. Quote a -> NormalizeTypeT m tyname uni ann a
MonadQuote
    )

-- | The constraints that type normalization requires.
type MonadNormalizeType uni m =
  ( MonadQuote m -- Type normalization must preserve global uniqueness.
  , HasUniApply uni -- See Note [Normalization of built-in types].
  )

-- | Run a 'NormalizeTypeT' computation.
runNormalizeTypeT :: NormalizeTypeT m tyname uni ann a -> m a
runNormalizeTypeT :: forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a -> m a
runNormalizeTypeT = (ReaderT (NormalizeTypeEnv tyname uni ann) m a
 -> NormalizeTypeEnv tyname uni ann -> m a)
-> NormalizeTypeEnv tyname uni ann
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
-> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT (NormalizeTypeEnv tyname uni ann) m a
-> NormalizeTypeEnv tyname uni ann -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (TypeVarEnv tyname uni ann -> NormalizeTypeEnv tyname uni ann
forall tyname (uni :: * -> *) ann.
TypeVarEnv tyname uni ann -> NormalizeTypeEnv tyname uni ann
NormalizeTypeEnv TypeVarEnv tyname uni ann
forall a. Monoid a => a
mempty) (ReaderT (NormalizeTypeEnv tyname uni ann) m a -> m a)
-> (NormalizeTypeT m tyname uni ann a
    -> ReaderT (NormalizeTypeEnv tyname uni ann) m a)
-> NormalizeTypeT m tyname uni ann a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
forall (m :: * -> *) tyname (uni :: * -> *) ann a.
NormalizeTypeT m tyname uni ann a
-> ReaderT (NormalizeTypeEnv tyname uni ann) m a
unNormalizeTypeT

-- | Locally extend a 'TypeVarEnv' in a 'NormalizeTypeT' computation.
withExtendedTypeVarEnv ::
  (HasUnique tyname TypeUnique, Monad m) =>
  tyname ->
  Normalized (Type tyname uni ann) ->
  NormalizeTypeT m tyname uni ann a ->
  NormalizeTypeT m tyname uni ann a
withExtendedTypeVarEnv :: forall tyname (m :: * -> *) (uni :: * -> *) ann a.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
withExtendedTypeVarEnv tyname
name =
  (NormalizeTypeEnv tyname uni ann
 -> NormalizeTypeEnv tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall a.
(NormalizeTypeEnv tyname uni ann
 -> NormalizeTypeEnv tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((NormalizeTypeEnv tyname uni ann
  -> NormalizeTypeEnv tyname uni ann)
 -> NormalizeTypeT m tyname uni ann a
 -> NormalizeTypeT m tyname uni ann a)
-> (Normalized (Type tyname uni ann)
    -> NormalizeTypeEnv tyname uni ann
    -> NormalizeTypeEnv tyname uni ann)
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter
  (NormalizeTypeEnv tyname uni ann)
  (NormalizeTypeEnv tyname uni ann)
  (UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
  (UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> (UniqueMap
      TypeUnique (Dupable (Normalized (Type tyname uni ann)))
    -> UniqueMap
         TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter
  (NormalizeTypeEnv tyname uni ann)
  (NormalizeTypeEnv tyname uni ann)
  (UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
  (UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann))))
forall tyname (uni :: * -> *) ann tyname (uni :: * -> *) ann
       (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (TypeVarEnv tyname uni ann) (f (TypeVarEnv tyname uni ann))
-> p (NormalizeTypeEnv tyname uni ann)
     (f (NormalizeTypeEnv tyname uni ann))
normalizeTypeEnvTypeVarEnv ((UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))
  -> UniqueMap
       TypeUnique (Dupable (Normalized (Type tyname uni ann))))
 -> NormalizeTypeEnv tyname uni ann
 -> NormalizeTypeEnv tyname uni ann)
-> (Normalized (Type tyname uni ann)
    -> UniqueMap
         TypeUnique (Dupable (Normalized (Type tyname uni ann)))
    -> UniqueMap
         TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeEnv tyname uni ann
-> NormalizeTypeEnv tyname uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. tyname
-> Dupable (Normalized (Type tyname uni ann))
-> UniqueMap
     TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
     TypeUnique (Dupable (Normalized (Type tyname uni ann)))
forall name unique a.
HasUnique name unique =>
name -> a -> UniqueMap unique a -> UniqueMap unique a
insertByName tyname
name (Dupable (Normalized (Type tyname uni ann))
 -> UniqueMap
      TypeUnique (Dupable (Normalized (Type tyname uni ann)))
 -> UniqueMap
      TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> (Normalized (Type tyname uni ann)
    -> Dupable (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> UniqueMap
     TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> UniqueMap
     TypeUnique (Dupable (Normalized (Type tyname uni ann)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Normalized (Type tyname uni ann)
-> Dupable (Normalized (Type tyname uni ann))
forall a. a -> Dupable a
dupable

-- | Look up a @tyname@ in a 'TypeVarEnv'.
lookupTyNameM ::
  (HasUnique tyname TypeUnique, Monad m) =>
  tyname ->
  NormalizeTypeT m tyname uni ann (Maybe (Dupable (Normalized (Type tyname uni ann))))
lookupTyNameM :: forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Maybe (Dupable (Normalized (Type tyname uni ann))))
lookupTyNameM tyname
name = (NormalizeTypeEnv tyname uni ann
 -> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Maybe (Dupable (Normalized (Type tyname uni ann))))
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((NormalizeTypeEnv tyname uni ann
  -> Maybe (Dupable (Normalized (Type tyname uni ann))))
 -> NormalizeTypeT
      m
      tyname
      uni
      ann
      (Maybe (Dupable (Normalized (Type tyname uni ann)))))
-> (NormalizeTypeEnv tyname uni ann
    -> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Maybe (Dupable (Normalized (Type tyname uni ann))))
forall a b. (a -> b) -> a -> b
$ tyname
-> UniqueMap
     TypeUnique (Dupable (Normalized (Type tyname uni ann)))
-> Maybe (Dupable (Normalized (Type tyname uni ann)))
forall name unique a.
HasUnique name unique =>
name -> UniqueMap unique a -> Maybe a
lookupName tyname
name (UniqueMap TypeUnique (Dupable (Normalized (Type tyname uni ann)))
 -> Maybe (Dupable (Normalized (Type tyname uni ann))))
-> (NormalizeTypeEnv tyname uni ann
    -> UniqueMap
         TypeUnique (Dupable (Normalized (Type tyname uni ann))))
-> NormalizeTypeEnv tyname uni ann
-> Maybe (Dupable (Normalized (Type tyname uni ann)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NormalizeTypeEnv tyname uni ann
-> UniqueMap
     TypeUnique (Dupable (Normalized (Type tyname uni ann)))
forall tyname (uni :: * -> *) ann.
NormalizeTypeEnv tyname uni ann -> TypeVarEnv tyname uni ann
_normalizeTypeEnvTypeVarEnv

{- Note [Normalization]
Normalization works under the assumption that variables are globally unique.
We use environments instead of substitutions as they're more efficient.

Since all names are unique and there is no need to track scopes, type normalization has only two
interesting cases: function application and a variable usage. In the function application case we
normalize a function and its argument, add the normalized argument to the environment and continue
normalization. In the variable case we look up the variable in the current environment: if it's not
found, we leave the variable untouched. If the variable is found, then what this variable stands for
was previously added to an environment (while handling the function application case), so we pick
this value and rename all bound variables in it to preserve the global uniqueness condition. It is
safe to do so, because picked values cannot contain uninstantiated variables as only normalized
types are added to environments and normalization instantiates all variables presented in an
environment.

See also Note [Normalization of built-in types].
-}

{- Note [Normalization of built-in types]
Instantiating a polymorphic built-in type amounts to applying it to some arguments. However,
the notion of "applying" is ambiguous, it can mean one of these two things:

1. lifting the built-in type to 'Type' and applying that via 'TyApp'
2. applying the built-in type right inside the universe to get a monomorphized type tag
   (e.g. the default universe has 'DefaultUniApply' for that purpose)

We need both of these things. The former allows us to assign types to polymorphic built-in functions
(otherwise applying a built-in type to a type variable would be unrepresentable), the latter is
used at runtime to juggle type tags so that we can avoid @unsafeCoerce@-ing, bring instances in
scope via 'bring' etc -- for all of that we have to have fully monomorphized type tags at runtime.

So in order for type checking to work we need to normalize polymorphic built-in types. For that
we simply turn intra-universe applications into regular type applications during type normalization.

We could go the other way around and "reduce" regular type applications into intra-universe ones,
however that would be harder to implement, because collapsing a general 'Type' into a 'SomeTypeIn'
is harder than expanding a 'SomeTypeIn' into a 'Type'. And it would also be impossible to do in the
general case, 'cause you can't collapse an application of a built-in type to, say, a type variable
into an intra-universe application as there are no type variables there. I guess we could "reduce"
application of built-in types in some cases and not reduce them in others and still make the whole
thing work, but that requires substantially more logic and is also a lot harder to get right.
Hence we do the opposite, which is straightforward.
-}

-- See Note [Normalization of built-in types].

{- | Normalize a built-in type by replacing each application inside the universe with regular
type application.
-}
normalizeUni :: forall k (a :: k) uni tyname. HasUniApply uni => uni (Esc a) -> Type tyname uni ()
normalizeUni :: forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc a)
uni =
  uni (Esc a)
-> Type tyname uni ()
-> (forall k l (f :: k -> l) (a :: k).
    (Esc a ~ Esc (f a)) =>
    uni (Esc f) -> uni (Esc a) -> Type tyname uni ())
-> Type tyname uni ()
forall tb r.
uni tb
-> r
-> (forall k l (f :: k -> l) (a :: k).
    (tb ~ Esc (f a)) =>
    uni (Esc f) -> uni (Esc a) -> r)
-> r
forall (uni :: * -> *) tb r.
HasUniApply uni =>
uni tb
-> r
-> (forall k l (f :: k -> l) (a :: k).
    (tb ~ Esc (f a)) =>
    uni (Esc f) -> uni (Esc a) -> r)
-> r
matchUniApply
    uni (Esc a)
uni
    -- If @uni@ is not an intra-universe application, then we're done.
    (() -> uni (Esc a) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf () uni (Esc a)
uni)
    -- If it is, then we turn that application into normal type application and recurse
    -- into both the function and its argument.
    (\uni (Esc f)
uniF uni (Esc a)
uniA -> ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (uni (Esc f) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc f)
uniF) (Type tyname uni () -> Type tyname uni ())
-> Type tyname uni () -> Type tyname uni ()
forall a b. (a -> b) -> a -> b
$ uni (Esc a) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc a)
uniA)

-- See Note [Normalization].

-- | Normalize a 'Type' in the 'NormalizeTypeT' monad.
normalizeTypeM ::
  (HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
  Type tyname uni ann ->
  NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM :: forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM (TyForall ann
ann tyname
name Kind ann
kind Type tyname uni ann
body) =
  ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
name Kind ann
kind (Type tyname uni ann -> Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
body
normalizeTypeM (TyIFix ann
ann Type tyname uni ann
pat Type tyname uni ann
arg) =
  ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Normalized (Type tyname uni ann -> Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
pat NormalizeTypeT
  m
  tyname
  uni
  ann
  (Normalized (Type tyname uni ann -> Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
arg
normalizeTypeM (TyFun ann
ann Type tyname uni ann
dom Type tyname uni ann
cod) =
  ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Normalized (Type tyname uni ann -> Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
dom NormalizeTypeT
  m
  tyname
  uni
  ann
  (Normalized (Type tyname uni ann -> Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Applicative f1, Applicative f2) =>
f1 (f2 (a -> b)) -> f1 (f2 a) -> f1 (f2 b)
<<*>> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
cod
normalizeTypeM (TyLam ann
ann tyname
name Kind ann
kind Type tyname uni ann
body) =
  ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann tyname
name Kind ann
kind (Type tyname uni ann -> Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(Functor f1, Functor f2) =>
(a -> b) -> f1 (f2 a) -> f1 (f2 b)
<<$>> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
body
normalizeTypeM (TyApp ann
ann Type tyname uni ann
fun Type tyname uni ann
arg) = do
  Normalized (Type tyname uni ann)
vFun <- Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
fun
  Normalized (Type tyname uni ann)
vArg <- Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM Type tyname uni ann
arg
  case Normalized (Type tyname uni ann) -> Type tyname uni ann
forall a. Normalized a -> a
unNormalized Normalized (Type tyname uni ann)
vFun of
    TyLam ann
_ tyname
nArg Kind ann
_ Type tyname uni ann
body -> Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
substNormalizeTypeM Normalized (Type tyname uni ann)
vArg tyname
nArg Type tyname uni ann
body
    Type tyname uni ann
_                   -> Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
 -> NormalizeTypeT
      m tyname uni ann (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> Normalized (Type tyname uni ann)
-> Normalized (Type tyname uni ann -> Type tyname uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Normalized (Type tyname uni ann)
vFun Normalized (Type tyname uni ann -> Type tyname uni ann)
-> Normalized (Type tyname uni ann)
-> Normalized (Type tyname uni ann)
forall a b. Normalized (a -> b) -> Normalized a -> Normalized b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Normalized (Type tyname uni ann)
vArg
normalizeTypeM var :: Type tyname uni ann
var@(TyVar ann
_ tyname
name) = do
  Maybe (Dupable (Normalized (Type tyname uni ann)))
mayTy <- tyname
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Maybe (Dupable (Normalized (Type tyname uni ann))))
forall tyname (m :: * -> *) (uni :: * -> *) ann.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> NormalizeTypeT
     m
     tyname
     uni
     ann
     (Maybe (Dupable (Normalized (Type tyname uni ann))))
lookupTyNameM tyname
name
  case Maybe (Dupable (Normalized (Type tyname uni ann)))
mayTy of
    -- A variable is always normalized.
    Maybe (Dupable (Normalized (Type tyname uni ann)))
Nothing -> Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
 -> NormalizeTypeT
      m tyname uni ann (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a. a -> Normalized a
Normalized Type tyname uni ann
var
    Just Dupable (Normalized (Type tyname uni ann))
ty -> Dupable (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall (m :: * -> *) a.
(MonadQuote m, Rename a) =>
Dupable a -> m a
liftDupable Dupable (Normalized (Type tyname uni ann))
ty
normalizeTypeM (TyBuiltin ann
ann (SomeTypeIn uni (Esc a)
uni)) =
  Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
 -> NormalizeTypeT
      m tyname uni ann (Normalized (Type tyname uni ann)))
-> (Type tyname uni ann -> Normalized (Type tyname uni ann))
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a. a -> Normalized a
Normalized (Type tyname uni ann
 -> NormalizeTypeT
      m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ ann
ann ann -> Type tyname uni () -> Type tyname uni ann
forall a b. a -> Type tyname uni b -> Type tyname uni a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ uni (Esc a) -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname.
HasUniApply uni =>
uni (Esc a) -> Type tyname uni ()
normalizeUni uni (Esc a)
uni
normalizeTypeM (TySOP ann
ann [[Type tyname uni ann]]
tyls) = do
  [[Type tyname uni ann]]
tyls' <- (([Type tyname uni ann]
 -> NormalizeTypeT m tyname uni ann [Type tyname uni ann])
-> [[Type tyname uni ann]]
-> NormalizeTypeT m tyname uni ann [[Type tyname uni ann]]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (([Type tyname uni ann]
  -> NormalizeTypeT m tyname uni ann [Type tyname uni ann])
 -> [[Type tyname uni ann]]
 -> NormalizeTypeT m tyname uni ann [[Type tyname uni ann]])
-> ((Type tyname uni ann
     -> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
    -> [Type tyname uni ann]
    -> NormalizeTypeT m tyname uni ann [Type tyname uni ann])
-> (Type tyname uni ann
    -> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> [[Type tyname uni ann]]
-> NormalizeTypeT m tyname uni ann [[Type tyname uni ann]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni ann
 -> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> [Type tyname uni ann]
-> NormalizeTypeT m tyname uni ann [Type tyname uni ann]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse) ((Normalized (Type tyname uni ann) -> Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Normalized (Type tyname uni ann) -> Type tyname uni ann
forall a. Normalized a -> a
unNormalized (NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
 -> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> (Type tyname uni ann
    -> NormalizeTypeT
         m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM) [[Type tyname uni ann]]
tyls
  Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a. a -> NormalizeTypeT m tyname uni ann a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Normalized (Type tyname uni ann)
 -> NormalizeTypeT
      m tyname uni ann (Normalized (Type tyname uni ann)))
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall a b. (a -> b) -> a -> b
$ Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a. a -> Normalized a
Normalized (Type tyname uni ann -> Normalized (Type tyname uni ann))
-> Type tyname uni ann -> Normalized (Type tyname uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> [[Type tyname uni ann]] -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP ann
ann [[Type tyname uni ann]]
tyls'

{- Note [Normalizing substitution]
@substituteNormalizeM@ is only ever used as normalizing substitution that receives two already
normalized types. However we do not enforce this in the type signature, because
1) it's perfectly correct for the last argument to be non-normalized
2) it would be annoying to wrap 'Type's into 'NormalizedType's
-}

-- See Note [Normalizing substitution].
-- | Substitute a type for a variable in a type and normalize in the 'NormalizeTypeT' monad.
substNormalizeTypeM ::
  (HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
  -- | @ty@
  Normalized (Type tyname uni ann) ->
  -- | @name@
  tyname ->
  -- | @body@
  Type tyname uni ann ->
  -- | @NORM ([ty / name] body)@
  NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
substNormalizeTypeM :: forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Normalized (Type tyname uni ann)
-> tyname
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
substNormalizeTypeM Normalized (Type tyname uni ann)
ty tyname
name = tyname
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (m :: * -> *) (uni :: * -> *) ann a.
(HasUnique tyname TypeUnique, Monad m) =>
tyname
-> Normalized (Type tyname uni ann)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann a
withExtendedTypeVarEnv tyname
name Normalized (Type tyname uni ann)
ty (NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
 -> NormalizeTypeT
      m tyname uni ann (Normalized (Type tyname uni ann)))
-> (Type tyname uni ann
    -> NormalizeTypeT
         m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM

-- | Normalize every 'Type' in a 'Term'.
normalizeTypesInM ::
  (HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
  Term tyname name uni fun ann ->
  NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeTypesInM :: forall tyname (uni :: * -> *) (m :: * -> *) name fun ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeTypesInM = LensLike
  (WrappedMonad (NormalizeTypeT m tyname uni ann))
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
-> (Term tyname name uni fun ann
    -> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann))
-> Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
forall (m :: * -> *) a b.
Monad m =>
LensLike (WrappedMonad m) a b a b -> (b -> m b) -> a -> m b
transformMOf LensLike
  (WrappedMonad (NormalizeTypeT m tyname uni ann))
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
  (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Term tyname name uni fun ann -> f (Term tyname name uni fun ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubterms Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
forall {name} {fun} {ann}.
Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeChildTypes
  where
    normalizeChildTypes :: Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
normalizeChildTypes = (Type tyname uni ann
 -> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> Term tyname name uni fun ann
-> NormalizeTypeT m tyname uni ann (Term tyname name uni fun ann)
forall tyname name (uni :: * -> *) fun ann (f :: * -> *).
Applicative f =>
(Type tyname uni ann -> f (Type tyname uni ann))
-> Term tyname name uni fun ann -> f (Term tyname name uni fun ann)
termSubtypes ((Normalized (Type tyname uni ann) -> Type tyname uni ann)
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall a b.
(a -> b)
-> NormalizeTypeT m tyname uni ann a
-> NormalizeTypeT m tyname uni ann b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Normalized (Type tyname uni ann) -> Type tyname uni ann
forall a. Normalized a -> a
unNormalized (NormalizeTypeT m tyname uni ann (Normalized (Type tyname uni ann))
 -> NormalizeTypeT m tyname uni ann (Type tyname uni ann))
-> (Type tyname uni ann
    -> NormalizeTypeT
         m tyname uni ann (Normalized (Type tyname uni ann)))
-> Type tyname uni ann
-> NormalizeTypeT m tyname uni ann (Type tyname uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann
-> NormalizeTypeT
     m tyname uni ann (Normalized (Type tyname uni ann))
normalizeTypeM)