    {-|
      Copyright   :  (C) 2012-2016, University of Twente,
                         2016     , Myrtle Software Ltd,
                         2017     , Google Inc.
                         2021     , QBayLogic B.V.
      License     :  BSD2 (see the file LICENSE)
      Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>

      Types in CoreHW
    -}

    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE FlexibleInstances #-}
    {-# LANGUAGE MagicHash #-}
    {-# LANGUAGE MultiParamTypeClasses #-}
    {-# LANGUAGE NamedFieldPuns #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE UndecidableInstances #-}

    module Clash.Core.Type
      ( Type (..)
      , TypeView (..)
      , ConstTy (..)
      , LitTy (..)
      , Kind
      , KindOrType
      , KiName
      , TyName
      , TyVar
      , tyView
      , coreView
      , coreView1
      , mkTyConTy
      , mkFunTy
      , mkPolyFunTy
      , mkTyConApp
      , splitFunTy
      , splitFunTys
      , splitFunForallTy
      , splitCoreFunForallTy
      , splitTyConAppM
      , isPolyFunTy
      , isPolyFunCoreTy
      , isPolyTy
      , isTypeFamilyApplication
      , isFunTy
      , isClassTy
      , applyFunTy
      , findFunSubst
      , reduceTypeFamily
      , isIntegerTy
      , normalizeType
      , varAttrs
      , typeAttrs
      )
    where

    -- External import
    import           Control.DeepSeq        as DS
    import           Data.Binary            (Binary)
    import           Data.Coerce            (coerce)
    import           Data.Hashable          (Hashable (hashWithSalt))
    import           Data.List              (foldl')
    import           Data.List.Extra        (splitAtList)
    import           Data.Maybe             (isJust, mapMaybe)
    import           Data.Text              (Text)
    import           GHC.Base               (isTrue#,(==#))
    import           GHC.Generics           (Generic(..))
    import           GHC.Integer            (smallInteger)
    import           GHC.Integer.Logarithms (integerLogBase#)
    import           GHC.TypeLits           (type TypeError, ErrorMessage(Text, (:<>:)))
    #if MIN_VERSION_base(4,16,0)
    import           GHC.Base               (ord)
    import           Data.Char              (chr)
    import           Data.Maybe             (fromMaybe)
    import           Data.Text.Extra        (showt)
    #endif

    -- GHC API
    #if MIN_VERSION_ghc(9,0,0)
    #if MIN_VERSION_ghc(9,2,0)
    import           GHC.Builtin.Names
      (typeCharCmpTyFamNameKey, typeConsSymbolTyFamNameKey, typeUnconsSymbolTyFamNameKey,
       typeCharToNatTyFamNameKey, typeNatToCharTyFamNameKey)
    #else
    import           GHC.Builtin.Names      (typeNatLeqTyFamNameKey)
    #endif
    import           GHC.Builtin.Names
      (integerTyConKey, typeNatAddTyFamNameKey, typeNatExpTyFamNameKey,
       typeNatMulTyFamNameKey, typeNatSubTyFamNameKey,
       typeNatCmpTyFamNameKey, ordLTDataConKey, ordEQDataConKey, ordGTDataConKey,
       typeSymbolAppendFamNameKey, typeSymbolCmpTyFamNameKey)
    import           GHC.Types.SrcLoc       (wiredInSrcSpan)
    import           GHC.Types.Unique       (getKey)
    #else
    #if __GLASGOW_HASKELL__ >= 808
    import           PrelNames
      (ordLTDataConKey, ordEQDataConKey, ordGTDataConKey)
    #else
    import           Unique                 (Unique)
    import           PrelNames
      (ltDataConKey, eqDataConKey, gtDataConKey)
    #endif
    import           PrelNames
      (integerTyConKey, typeNatAddTyFamNameKey, typeNatExpTyFamNameKey,
       typeNatLeqTyFamNameKey, typeNatMulTyFamNameKey, typeNatSubTyFamNameKey,
       typeNatCmpTyFamNameKey,
       typeSymbolAppendFamNameKey, typeSymbolCmpTyFamNameKey)
    import           SrcLoc                 (wiredInSrcSpan)
    import           Unique                 (getKey)
    #endif

    -- Local imports
    import           Clash.Annotations.SynthesisAttributes
    import           Clash.Core.DataCon
    import           Clash.Core.Name
    import {-# SOURCE #-} Clash.Core.Subst
    import           Clash.Core.TyCon
    import           Clash.Core.Var
    import qualified Clash.Data.UniqMap as UniqMap
    import           Clash.Util

    #if __GLASGOW_HASKELL__ <= 806
    ordLTDataConKey, ordEQDataConKey, ordGTDataConKey :: Unique.Unique
    ordLTDataConKey = ltDataConKey
    ordEQDataConKey = eqDataConKey
    ordGTDataConKey = gtDataConKey
    #endif

    varAttrs :: Var a -> [Attr Text]
    varAttrs :: forall a. Var a -> [Attr OccName]
    varAttrs t :: Var a
    t@(TyVar {}) =
      String -> [Attr OccName]
    forall a. HasCallStack => String -> a
    error (String -> [Attr OccName]) -> String -> [Attr OccName]
    forall a b. (a -> b) -> a -> b
    $ $(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "Unexpected argument: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Var a -> String
    forall a. Show a => a -> String
    show Var a
    t

    varAttrs (Id Name a
    _ Unique
    _ Type
    ty IdScope
    _) =
      case Type
    ty of
        AnnType [Attr OccName]
    attrs Type
    _typ -> [Attr OccName]
    attrs
        Type
    _                  -> []

    -- | Types in CoreHW: function and polymorphic types
    data Type
      = VarTy    !TyVar             -- ^ Type variable
      | ConstTy  !ConstTy           -- ^ Type constant
      | ForAllTy !TyVar !Type       -- ^ Polymorphic Type
      | AppTy    !Type !Type        -- ^ Type Application
      | LitTy    !LitTy             -- ^ Type literal
      | AnnType  [Attr Text] !Type  -- ^ Annotated type, see Clash.Annotations.SynthesisAttributes
      deriving (Unique -> Type -> String -> String
    [Type] -> String -> String
    Type -> String
    (Unique -> Type -> String -> String)
    -> (Type -> String) -> ([Type] -> String -> String) -> Show Type
    forall a.
    (Unique -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Unique -> Type -> String -> String
    showsPrec :: Unique -> Type -> String -> String
    $cshow :: Type -> String
    show :: Type -> String
    $cshowList :: [Type] -> String -> String
    showList :: [Type] -> String -> String
    Show, (forall x. Type -> Rep Type x)
    -> (forall x. Rep Type x -> Type) -> Generic Type
    forall x. Rep Type x -> Type
    forall x. Type -> Rep Type x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Type -> Rep Type x
    from :: forall x. Type -> Rep Type x
    $cto :: forall x. Rep Type x -> Type
    to :: forall x. Rep Type x -> Type
    Generic, Type -> ()
    (Type -> ()) -> NFData Type
    forall a. (a -> ()) -> NFData a
    $crnf :: Type -> ()
    rnf :: Type -> ()
    NFData, Get Type
    [Type] -> Put
    Type -> Put
    (Type -> Put) -> Get Type -> ([Type] -> Put) -> Binary Type
    forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
    $cput :: Type -> Put
    put :: Type -> Put
    $cget :: Get Type
    get :: Get Type
    $cputList :: [Type] -> Put
    putList :: [Type] -> Put
    Binary)

    instance TypeError (
            'Text "A broken implementation of Hashable Type has been "
      ':<>: 'Text "removed in Clash 1.4.7. If this is an issue for you, please submit "
      ':<>: 'Text "an issue report at https://github.com/clash-lang/clash-compiler/issues."
      ) => Hashable Type where
        hashWithSalt :: Unique -> Type -> Unique
    hashWithSalt = String -> Unique -> Type -> Unique
    forall a. HasCallStack => String -> a
    error String
    "Type.hashWithSalt: unreachable"

    -- | An easier view on types
    data TypeView
      = FunTy    !Type  !Type      -- ^ Function type
      | TyConApp !TyConName [Type] -- ^ Applied TyCon
      | OtherType !Type            -- ^ Neither of the above
      deriving Unique -> TypeView -> String -> String
    [TypeView] -> String -> String
    TypeView -> String
    (Unique -> TypeView -> String -> String)
    -> (TypeView -> String)
    -> ([TypeView] -> String -> String)
    -> Show TypeView
    forall a.
    (Unique -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Unique -> TypeView -> String -> String
    showsPrec :: Unique -> TypeView -> String -> String
    $cshow :: TypeView -> String
    show :: TypeView -> String
    $cshowList :: [TypeView] -> String -> String
    showList :: [TypeView] -> String -> String
    Show

    -- | Type Constants
    data ConstTy
      = TyCon !TyConName -- ^ TyCon type
      | Arrow            -- ^ Function type
      deriving (ConstTy -> ConstTy -> Bool
    (ConstTy -> ConstTy -> Bool)
    -> (ConstTy -> ConstTy -> Bool) -> Eq ConstTy
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ConstTy -> ConstTy -> Bool
    == :: ConstTy -> ConstTy -> Bool
    $c/= :: ConstTy -> ConstTy -> Bool
    /= :: ConstTy -> ConstTy -> Bool
    Eq,Eq ConstTy
    Eq ConstTy =>
    (ConstTy -> ConstTy -> Ordering)
    -> (ConstTy -> ConstTy -> Bool)
    -> (ConstTy -> ConstTy -> Bool)
    -> (ConstTy -> ConstTy -> Bool)
    -> (ConstTy -> ConstTy -> Bool)
    -> (ConstTy -> ConstTy -> ConstTy)
    -> (ConstTy -> ConstTy -> ConstTy)
    -> Ord ConstTy
    ConstTy -> ConstTy -> Bool
    ConstTy -> ConstTy -> Ordering
    ConstTy -> ConstTy -> ConstTy
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: ConstTy -> ConstTy -> Ordering
    compare :: ConstTy -> ConstTy -> Ordering
    $c< :: ConstTy -> ConstTy -> Bool
    < :: ConstTy -> ConstTy -> Bool
    $c<= :: ConstTy -> ConstTy -> Bool
    <= :: ConstTy -> ConstTy -> Bool
    $c> :: ConstTy -> ConstTy -> Bool
    > :: ConstTy -> ConstTy -> Bool
    $c>= :: ConstTy -> ConstTy -> Bool
    >= :: ConstTy -> ConstTy -> Bool
    $cmax :: ConstTy -> ConstTy -> ConstTy
    max :: ConstTy -> ConstTy -> ConstTy
    $cmin :: ConstTy -> ConstTy -> ConstTy
    min :: ConstTy -> ConstTy -> ConstTy
    Ord,Unique -> ConstTy -> String -> String
    [ConstTy] -> String -> String
    ConstTy -> String
    (Unique -> ConstTy -> String -> String)
    -> (ConstTy -> String)
    -> ([ConstTy] -> String -> String)
    -> Show ConstTy
    forall a.
    (Unique -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Unique -> ConstTy -> String -> String
    showsPrec :: Unique -> ConstTy -> String -> String
    $cshow :: ConstTy -> String
    show :: ConstTy -> String
    $cshowList :: [ConstTy] -> String -> String
    showList :: [ConstTy] -> String -> String
    Show,(forall x. ConstTy -> Rep ConstTy x)
    -> (forall x. Rep ConstTy x -> ConstTy) -> Generic ConstTy
    forall x. Rep ConstTy x -> ConstTy
    forall x. ConstTy -> Rep ConstTy x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. ConstTy -> Rep ConstTy x
    from :: forall x. ConstTy -> Rep ConstTy x
    $cto :: forall x. Rep ConstTy x -> ConstTy
    to :: forall x. Rep ConstTy x -> ConstTy
    Generic,ConstTy -> ()
    (ConstTy -> ()) -> NFData ConstTy
    forall a. (a -> ()) -> NFData a
    $crnf :: ConstTy -> ()
    rnf :: ConstTy -> ()
    NFData,Eq ConstTy
    Eq ConstTy =>
    (Unique -> ConstTy -> Unique)
    -> (ConstTy -> Unique) -> Hashable ConstTy
    Unique -> ConstTy -> Unique
    ConstTy -> Unique
    forall a.
    Eq a =>
    (Unique -> a -> Unique) -> (a -> Unique) -> Hashable a
    $chashWithSalt :: Unique -> ConstTy -> Unique
    hashWithSalt :: Unique -> ConstTy -> Unique
    $chash :: ConstTy -> Unique
    hash :: ConstTy -> Unique
    Hashable,Get ConstTy
    [ConstTy] -> Put
    ConstTy -> Put
    (ConstTy -> Put)
    -> Get ConstTy -> ([ConstTy] -> Put) -> Binary ConstTy
    forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
    $cput :: ConstTy -> Put
    put :: ConstTy -> Put
    $cget :: Get ConstTy
    get :: Get ConstTy
    $cputList :: [ConstTy] -> Put
    putList :: [ConstTy] -> Put
    Binary)

    -- | Literal Types
    data LitTy
      = NumTy !Integer
      | SymTy !String
      | CharTy !Char
      deriving (LitTy -> LitTy -> Bool
    (LitTy -> LitTy -> Bool) -> (LitTy -> LitTy -> Bool) -> Eq LitTy
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: LitTy -> LitTy -> Bool
    == :: LitTy -> LitTy -> Bool
    $c/= :: LitTy -> LitTy -> Bool
    /= :: LitTy -> LitTy -> Bool
    Eq,Eq LitTy
    Eq LitTy =>
    (LitTy -> LitTy -> Ordering)
    -> (LitTy -> LitTy -> Bool)
    -> (LitTy -> LitTy -> Bool)
    -> (LitTy -> LitTy -> Bool)
    -> (LitTy -> LitTy -> Bool)
    -> (LitTy -> LitTy -> LitTy)
    -> (LitTy -> LitTy -> LitTy)
    -> Ord LitTy
    LitTy -> LitTy -> Bool
    LitTy -> LitTy -> Ordering
    LitTy -> LitTy -> LitTy
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: LitTy -> LitTy -> Ordering
    compare :: LitTy -> LitTy -> Ordering
    $c< :: LitTy -> LitTy -> Bool
    < :: LitTy -> LitTy -> Bool
    $c<= :: LitTy -> LitTy -> Bool
    <= :: LitTy -> LitTy -> Bool
    $c> :: LitTy -> LitTy -> Bool
    > :: LitTy -> LitTy -> Bool
    $c>= :: LitTy -> LitTy -> Bool
    >= :: LitTy -> LitTy -> Bool
    $cmax :: LitTy -> LitTy -> LitTy
    max :: LitTy -> LitTy -> LitTy
    $cmin :: LitTy -> LitTy -> LitTy
    min :: LitTy -> LitTy -> LitTy
    Ord,Unique -> LitTy -> String -> String
    [LitTy] -> String -> String
    LitTy -> String
    (Unique -> LitTy -> String -> String)
    -> (LitTy -> String) -> ([LitTy] -> String -> String) -> Show LitTy
    forall a.
    (Unique -> a -> String -> String)
    -> (a -> String) -> ([a] -> String -> String) -> Show a
    $cshowsPrec :: Unique -> LitTy -> String -> String
    showsPrec :: Unique -> LitTy -> String -> String
    $cshow :: LitTy -> String
    show :: LitTy -> String
    $cshowList :: [LitTy] -> String -> String
    showList :: [LitTy] -> String -> String
    Show,(forall x. LitTy -> Rep LitTy x)
    -> (forall x. Rep LitTy x -> LitTy) -> Generic LitTy
    forall x. Rep LitTy x -> LitTy
    forall x. LitTy -> Rep LitTy x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. LitTy -> Rep LitTy x
    from :: forall x. LitTy -> Rep LitTy x
    $cto :: forall x. Rep LitTy x -> LitTy
    to :: forall x. Rep LitTy x -> LitTy
    Generic,LitTy -> ()
    (LitTy -> ()) -> NFData LitTy
    forall a. (a -> ()) -> NFData a
    $crnf :: LitTy -> ()
    rnf :: LitTy -> ()
    NFData,Eq LitTy
    Eq LitTy =>
    (Unique -> LitTy -> Unique) -> (LitTy -> Unique) -> Hashable LitTy
    Unique -> LitTy -> Unique
    LitTy -> Unique
    forall a.
    Eq a =>
    (Unique -> a -> Unique) -> (a -> Unique) -> Hashable a
    $chashWithSalt :: Unique -> LitTy -> Unique
    hashWithSalt :: Unique -> LitTy -> Unique
    $chash :: LitTy -> Unique
    hash :: LitTy -> Unique
    Hashable,Get LitTy
    [LitTy] -> Put
    LitTy -> Put
    (LitTy -> Put) -> Get LitTy -> ([LitTy] -> Put) -> Binary LitTy
    forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
    $cput :: LitTy -> Put
    put :: LitTy -> Put
    $cget :: Get LitTy
    get :: Get LitTy
    $cputList :: [LitTy] -> Put
    putList :: [LitTy] -> Put
    Binary)

    -- | The level above types
    type Kind       = Type
    -- | Either a Kind or a Type
    type KindOrType = Type

    -- | Reference to a Type
    type TyName     = Name Type
    -- | Reference to a Kind
    type KiName     = Name Kind

    -- TODO
    --
    -- tyView could be smarter about what it gives back. Since it traverses the
    -- arguments to make a `TyConApp`, if the leftmost innermost type isn't a
    -- TyCon it could still return a list of applied types to save a later call to
    -- something like splitFunForallTy.
    --
    -- It could / should also look through annotations instead of just returning
    -- the original type wrapped in OtherType.

    -- | An easier view on types
    --
    -- Note [Arrow arguments]
    --
    -- Clash' Arrow type can either have 2 or 4 arguments, depending on who created it.
    -- By default it has two arguments: the argument type of a function, and the result
    -- type of a function.
    --
    -- So when do we have 4 arguments? When in Haskell/GHC land the arrow was
    -- unsaturated. This can happen in instance heads, or in the eta-reduced
    -- representation of newtypes. So what are those additional 2 arguments compared to
    -- the "normal" function type? They're the kinds of argument and result type.
    tyView :: Type -> TypeView
    -- XXX: this is a manually unrolled version of:
    --
    -- tyView tOrig = go [] tOrig
    --  where
    --   go args t = case t of
    --     ConstTy c -> case c of
    --       TyCon tc -> TyConApp tc args
    --       Arrow -> case args of
    --         (arg:res:rest) -> case rest of
    --           [] -> FunTy arg res
    --           [arg1,res1] -> FunTy arg1 res1
    --           _ -> OtherType tOrig
    --     AppTy l r -> go (r:args) l
    --     _ -> OtherType tOrig
    --
    -- To get a FunTy without recursive calls. Because it is called so often this
    -- saves us 5-10% runtime.
    tyView :: Type -> TypeView
    tyView Type
    tOrig = case Type
    tOrig of
      ConstTy ConstTy
    c -> case ConstTy
    c of
        TyCon TyConName
    tc -> TyConName -> [Type] -> TypeView
    TyConApp TyConName
    tc []
        ConstTy
    _ -> Type -> TypeView
    OtherType Type
    tOrig
      AppTy Type
    l0 Type
    res -> case Type
    l0 of
        ConstTy (TyCon TyConName
    tc) -> TyConName -> [Type] -> TypeView
    TyConApp TyConName
    tc [Type
    res]
        AppTy Type
    l1 Type
    arg -> case Type
    l1 of
          ConstTy ConstTy
    Arrow -> Type -> Type -> TypeView
    FunTy Type
    arg Type
    res
          ConstTy (TyCon TyConName
    tc) -> TyConName -> [Type] -> TypeView
    TyConApp TyConName
    tc [Type
    arg,Type
    res]
          AppTy Type
    l2 Type
    resK -> case Type
    l2 of
            ConstTy (TyCon TyConName
    tc) -> TyConName -> [Type] -> TypeView
    TyConApp TyConName
    tc [Type
    resK,Type
    arg,Type
    res]
            AppTy Type
    l3 Type
    argK -> case Type
    l3 of
              ConstTy (TyCon TyConName
    tc) -> TyConName -> [Type] -> TypeView
    TyConApp TyConName
    tc [Type
    argK,Type
    resK,Type
    arg,Type
    res]
              ConstTy ConstTy
    Arrow -> Type -> Type -> TypeView
    FunTy Type
    arg Type
    res -- See Note [Arrow arguments]
              Type
    _ -> case [Type] -> Type -> (Type, [Type])
    go [Type
    argK,Type
    resK,Type
    arg,Type
    res] Type
    l3 of
                (ConstTy (TyCon TyConName
    tc),[Type]
    args)
                  -> TyConName -> [Type] -> TypeView
    TyConApp TyConName
    tc [Type]
    args
                (Type, [Type])
    _ -> Type -> TypeView
    OtherType Type
    tOrig
            Type
    _ -> Type -> TypeView
    OtherType Type
    tOrig
          Type
    _ -> Type -> TypeView
    OtherType Type
    tOrig
        Type
    _ -> Type -> TypeView
    OtherType Type
    tOrig
      Type
    _ -> Type -> TypeView
    OtherType Type
    tOrig
     where
      go :: [Type] -> Type -> (Type, [Type])
    go [Type]
    args (AppTy Type
    ty1 Type
    ty2) = [Type] -> Type -> (Type, [Type])
    go (Type
    ty2Type -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    args) Type
    ty1
      go [Type]
    args Type
    t1              = (Type
    t1,[Type]
    args)

    -- | A view on types in which newtypes are transparent, the Signal type is
    -- transparent, and type functions are evaluated to WHNF (when possible).
    --
    -- Strips away ALL layers. If no layers are found it returns the given type.
    coreView :: TyConMap -> Type -> Type
    coreView :: TyConMap -> Type -> Type
    coreView TyConMap
    tcm Type
    ty =
      case TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    tcm Type
    ty of
        Maybe Type
    Nothing  -> Type
    ty
        Just Type
    ty' -> TyConMap -> Type -> Type
    coreView TyConMap
    tcm Type
    ty'

    -- | A view on types in which newtypes are transparent, the Signal type is
    -- transparent, and type functions are evaluated to WHNF (when possible).
    --
    -- Only strips away one "layer".
    coreView1 :: TyConMap -> Type -> Maybe Type
    coreView1 :: TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    tcMap Type
    ty = case Type -> TypeView
    tyView Type
    ty of
      TyConApp TyConName
    tcNm [Type]
    args
        | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Signal.BiSignal.BiSignalIn"
        , [Type
    _,Type
    _,Type
    _,Type
    elTy] <- [Type]
    args
        -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    elTy
        | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Signal.BiSignal.BiSignalOut"
        , [Type
    _,Type
    _,Type
    _,Type
    elTy] <- [Type]
    args
        -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    elTy
        | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Signal.Internal.Signal"
        , [Type
    _,Type
    elTy] <- [Type]
    args
        -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    elTy
        | Bool
    otherwise
        -> case TyConName -> TyConMap -> TyCon
    forall a b. Uniquable a => a -> UniqMap b -> b
    UniqMap.find TyConName
    tcNm TyConMap
    tcMap of
             AlgTyCon {algTcRhs :: TyCon -> AlgTyConRhs
    algTcRhs = (NewTyCon DataCon
    _ ([TyVar], Type)
    nt)}
               -> ([TyVar], Type) -> [Type] -> Maybe Type
    newTyConInstRhs ([TyVar], Type)
    nt [Type]
    args
             TyCon
    _ -> TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    tcMap Type
    ty
      OtherType (AnnType [Attr OccName]
    _ Type
    ty') -> TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    tcMap Type
    ty'
      TypeView
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

    -- | Instantiate and Apply the RHS/Original of a NewType with the given
    -- list of argument types
    --
    -- Returns /Nothing/ when under-applied
    newTyConInstRhs :: ([TyVar],Type) -> [Type] -> Maybe Type
    newTyConInstRhs :: ([TyVar], Type) -> [Type] -> Maybe Type
    newTyConInstRhs ([TyVar]
    tvs,Type
    ty) [Type]
    tys
        | [TyVar] -> Unique
    forall a. [a] -> Unique
    forall (t :: Type -> Type) a. Foldable t => t a -> Unique
    length [TyVar]
    tvs Unique -> Unique -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [Type] -> Unique
    forall a. [a] -> Unique
    forall (t :: Type -> Type) a. Foldable t => t a -> Unique
    length [Type]
    tys
        = Type -> Maybe Type
    forall a. a -> Maybe a
    Just ((Type -> Type -> Type) -> Type -> [Type] -> Type
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' Type -> Type -> Type
    AppTy (HasCallStack => [TyVar] -> [Type] -> Type -> Type
    [TyVar] -> [Type] -> Type -> Type
    substTyWith [TyVar]
    tvs [Type]
    tys1 Type
    ty) [Type]
    tys2)
        | Bool
    otherwise
        = Maybe Type
    forall a. Maybe a
    Nothing
      where
        ([Type]
    tys1, [Type]
    tys2) = [TyVar] -> [Type] -> ([Type], [Type])
    forall b a. [b] -> [a] -> ([a], [a])
    splitAtList [TyVar]
    tvs [Type]
    tys

    -- | Make a function type of an argument and result type
    mkFunTy :: Type -> Type -> Type
    mkFunTy :: Type -> Type -> Type
    mkFunTy Type
    t1 = Type -> Type -> Type
    AppTy (Type -> Type -> Type
    AppTy (ConstTy -> Type
    ConstTy ConstTy
    Arrow) Type
    t1)

    -- | Make a TyCon Application out of a TyCon and a list of argument types
    mkTyConApp :: TyConName -> [Type] -> Type
    mkTyConApp :: TyConName -> [Type] -> Type
    mkTyConApp TyConName
    tc = (Type -> Type -> Type) -> Type -> [Type] -> Type
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Type -> Type -> Type
    AppTy (ConstTy -> Type
    ConstTy (ConstTy -> Type) -> ConstTy -> Type
    forall a b. (a -> b) -> a -> b
    $ TyConName -> ConstTy
    TyCon TyConName
    tc)

    -- | Make a Type out of a TyCon
    mkTyConTy :: TyConName -> Type
    mkTyConTy :: TyConName -> Type
    mkTyConTy TyConName
    ty = ConstTy -> Type
    ConstTy (ConstTy -> Type) -> ConstTy -> Type
    forall a b. (a -> b) -> a -> b
    $ TyConName -> ConstTy
    TyCon TyConName
    ty

    -- | Split a TyCon Application in a TyCon and its arguments
    splitTyConAppM :: Type
                   -> Maybe (TyConName,[Type])
    splitTyConAppM :: Type -> Maybe (TyConName, [Type])
    splitTyConAppM (Type -> TypeView
    tyView -> TyConApp TyConName
    tc [Type]
    args) = (TyConName, [Type]) -> Maybe (TyConName, [Type])
    forall a. a -> Maybe a
    Just (TyConName
    tc,[Type]
    args)
    splitTyConAppM Type
    _                            = Maybe (TyConName, [Type])
    forall a. Maybe a
    Nothing

    -- | Is a type polymorphic?
    isPolyTy :: Type -> Bool
    isPolyTy :: Type -> Bool
    isPolyTy (ForAllTy TyVar
    _ Type
    _)          = Bool
    True
    isPolyTy (Type -> TypeView
    tyView -> FunTy Type
    _ Type
    res) = Type -> Bool
    isPolyTy Type
    res
    isPolyTy Type
    _                       = Bool
    False

    -- | Split a function type in an argument and result type
    splitFunTy :: TyConMap
               -> Type
               -> Maybe (Type, Type)
    splitFunTy :: TyConMap -> Type -> Maybe (Type, Type)
    splitFunTy TyConMap
    m (TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    m -> Just Type
    ty)  = TyConMap -> Type -> Maybe (Type, Type)
    splitFunTy TyConMap
    m Type
    ty
    splitFunTy TyConMap
    _ (Type -> TypeView
    tyView -> FunTy Type
    arg Type
    res) = (Type, Type) -> Maybe (Type, Type)
    forall a. a -> Maybe a
    Just (Type
    arg,Type
    res)
    splitFunTy TyConMap
    _ Type
    _ = Maybe (Type, Type)
    forall a. Maybe a
    Nothing

    splitFunTys :: TyConMap
                -> Type
                -> ([Type],Type)
    splitFunTys :: TyConMap -> Type -> ([Type], Type)
    splitFunTys TyConMap
    m Type
    ty = [Type] -> Type -> Type -> ([Type], Type)
    go [] Type
    ty Type
    ty
      where
        go :: [Type] -> Type -> Type -> ([Type], Type)
    go [Type]
    args Type
    orig_ty (TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    m -> Just Type
    ty') = [Type] -> Type -> Type -> ([Type], Type)
    go [Type]
    args Type
    orig_ty Type
    ty'
        go [Type]
    args Type
    _       (Type -> TypeView
    tyView -> FunTy Type
    arg Type
    res) = [Type] -> Type -> Type -> ([Type], Type)
    go (Type
    argType -> [Type] -> [Type]
    forall a. a -> [a] -> [a]
    :[Type]
    args) Type
    res Type
    res
        go [Type]
    args Type
    orig_ty Type
    _                         = ([Type] -> [Type]
    forall a. [a] -> [a]
    reverse [Type]
    args, Type
    orig_ty)

    -- | Split a poly-function type in a: list of type-binders and argument types,
    -- and the result type
    splitFunForallTy :: Type
                     -> ([Either TyVar Type],Type)
    splitFunForallTy :: Type -> ([Either TyVar Type], Type)
    splitFunForallTy = [Either TyVar Type] -> Type -> ([Either TyVar Type], Type)
    go []
      where
        go :: [Either TyVar Type] -> Type -> ([Either TyVar Type], Type)
    go [Either TyVar Type]
    args (ForAllTy TyVar
    tv Type
    ty)          = [Either TyVar Type] -> Type -> ([Either TyVar Type], Type)
    go (TyVar -> Either TyVar Type
    forall a b. a -> Either a b
    Left TyVar
    tvEither TyVar Type -> [Either TyVar Type] -> [Either TyVar Type]
    forall a. a -> [a] -> [a]
    :[Either TyVar Type]
    args) Type
    ty
        go [Either TyVar Type]
    args (Type -> TypeView
    tyView -> FunTy Type
    arg Type
    res) = [Either TyVar Type] -> Type -> ([Either TyVar Type], Type)
    go (Type -> Either TyVar Type
    forall a b. b -> Either a b
    Right Type
    argEither TyVar Type -> [Either TyVar Type] -> [Either TyVar Type]
    forall a. a -> [a] -> [a]
    :[Either TyVar Type]
    args) Type
    res
        go [Either TyVar Type]
    args Type
    ty                        = ([Either TyVar Type] -> [Either TyVar Type]
    forall a. [a] -> [a]
    reverse [Either TyVar Type]
    args,Type
    ty)

    -- | Make a polymorphic function type out of a result type and a list of
    -- quantifiers and function argument types
    mkPolyFunTy
      :: Type
      -- ^ Result type
      -> [Either TyVar Type]
      -- ^ List of quantifiers and function argument types
      -> Type
    mkPolyFunTy :: Type -> [Either TyVar Type] -> Type
    mkPolyFunTy = (Either TyVar Type -> Type -> Type)
    -> Type -> [Either TyVar Type] -> Type
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((TyVar -> Type -> Type)
    -> (Type -> Type -> Type) -> Either TyVar Type -> Type -> Type
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either TyVar -> Type -> Type
    ForAllTy Type -> Type -> Type
    mkFunTy)

    -- | Split a poly-function type in a: list of type-binders and argument types,
    -- and the result type. Looks through 'Signal' and type functions.
    splitCoreFunForallTy :: TyConMap
                         -> Type
                         -> ([Either TyVar Type], Type)
    splitCoreFunForallTy :: TyConMap -> Type -> ([Either TyVar Type], Type)
    splitCoreFunForallTy TyConMap
    tcm Type
    ty = [Either TyVar Type] -> Type -> Type -> ([Either TyVar Type], Type)
    go [] Type
    ty Type
    ty
      where
        go :: [Either TyVar Type] -> Type -> Type -> ([Either TyVar Type], Type)
    go [Either TyVar Type]
    args Type
    orig_ty (TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    tcm -> Just Type
    ty') = [Either TyVar Type] -> Type -> Type -> ([Either TyVar Type], Type)
    go [Either TyVar Type]
    args Type
    orig_ty Type
    ty'
        go [Either TyVar Type]
    args Type
    _       (ForAllTy TyVar
    tv Type
    res)           = [Either TyVar Type] -> Type -> Type -> ([Either TyVar Type], Type)
    go (TyVar -> Either TyVar Type
    forall a b. a -> Either a b
    Left TyVar
    tvEither TyVar Type -> [Either TyVar Type] -> [Either TyVar Type]
    forall a. a -> [a] -> [a]
    :[Either TyVar Type]
    args) Type
    res Type
    res
        go [Either TyVar Type]
    args Type
    _       (Type -> TypeView
    tyView -> FunTy Type
    arg Type
    res)   = [Either TyVar Type] -> Type -> Type -> ([Either TyVar Type], Type)
    go (Type -> Either TyVar Type
    forall a b. b -> Either a b
    Right Type
    argEither TyVar Type -> [Either TyVar Type] -> [Either TyVar Type]
    forall a. a -> [a] -> [a]
    :[Either TyVar Type]
    args) Type
    res Type
    res
        go [Either TyVar Type]
    args Type
    orig_ty Type
    _                           = ([Either TyVar Type] -> [Either TyVar Type]
    forall a. [a] -> [a]
    reverse [Either TyVar Type]
    args,Type
    orig_ty)

    -- | Is a type a polymorphic or function type?
    isPolyFunTy :: Type
                -> Bool
    isPolyFunTy :: Type -> Bool
    isPolyFunTy = Bool -> Bool
    not (Bool -> Bool) -> (Type -> Bool) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Either TyVar Type] -> Bool
    forall a. [a] -> Bool
    forall (t :: Type -> Type) a. Foldable t => t a -> Bool
    null ([Either TyVar Type] -> Bool)
    -> (Type -> [Either TyVar Type]) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Either TyVar Type], Type) -> [Either TyVar Type]
    forall a b. (a, b) -> a
    fst (([Either TyVar Type], Type) -> [Either TyVar Type])
    -> (Type -> ([Either TyVar Type], Type))
    -> Type
    -> [Either TyVar Type]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> ([Either TyVar Type], Type)
    splitFunForallTy

    -- | Is a type a polymorphic or function type under 'coreView1'?
    isPolyFunCoreTy :: TyConMap
                    -> Type
                    -> Bool
    isPolyFunCoreTy :: TyConMap -> Type -> Bool
    isPolyFunCoreTy TyConMap
    m (TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    m -> Just Type
    ty) = TyConMap -> Type -> Bool
    isPolyFunCoreTy TyConMap
    m Type
    ty
    isPolyFunCoreTy TyConMap
    _ Type
    ty = case Type -> TypeView
    tyView Type
    ty of
      FunTy Type
    _ Type
    _ -> Bool
    True
      OtherType (ForAllTy TyVar
    _ Type
    _) -> Bool
    True
      TypeView
    _ -> Bool
    False

    -- | Extract attributes from type. Will return an empty list if this is an
    -- AnnType with an empty list AND if this is not an AnnType at all.
    typeAttrs :: Type -> [Attr Text]
    typeAttrs :: Type -> [Attr OccName]
    typeAttrs (AnnType [Attr OccName]
    attrs Type
    _typ) = [Attr OccName]
    attrs
    typeAttrs Type
    _                    = []

    -- | Is a type a function type?
    isFunTy :: TyConMap
            -> Type
            -> Bool
    isFunTy :: TyConMap -> Type -> Bool
    isFunTy TyConMap
    m = Maybe (Type, Type) -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe (Type, Type) -> Bool)
    -> (Type -> Maybe (Type, Type)) -> Type -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TyConMap -> Type -> Maybe (Type, Type)
    splitFunTy TyConMap
    m

    -- | Apply a function type to an argument type and get the result type
    applyFunTy :: TyConMap
               -> Type
               -> Type
               -> Type
    applyFunTy :: TyConMap -> Type -> Type -> Type
    applyFunTy TyConMap
    m (TyConMap -> Type -> Maybe Type
    coreView1 TyConMap
    m -> Just Type
    ty)   Type
    arg = TyConMap -> Type -> Type -> Type
    applyFunTy TyConMap
    m Type
    ty Type
    arg
    applyFunTy TyConMap
    _ (Type -> TypeView
    tyView -> FunTy Type
    _ Type
    resTy) Type
    _    = Type
    resTy
    applyFunTy TyConMap
    _ Type
    _ Type
    _ = String -> Type
    forall a. HasCallStack => String -> a
    error (String -> Type) -> String -> Type
    forall a b. (a -> b) -> a -> b
    $ $(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "Report as bug: not a FunTy"

    -- Type function substitutions

    -- Given a set of type functions, and list of argument types, get the first
    -- type function that matches, and return its substituted RHS type.
    findFunSubst :: TyConMap -> [([Type],Type)] -> [Type] -> Maybe Type
    findFunSubst :: TyConMap -> [([Type], Type)] -> [Type] -> Maybe Type
    findFunSubst TyConMap
    _   [] [Type]
    _ = Maybe Type
    forall a. Maybe a
    Nothing
    findFunSubst TyConMap
    tcm (([Type], Type)
    tcSubst:[([Type], Type)]
    rest) [Type]
    args = case TyConMap -> ([Type], Type) -> [Type] -> Maybe Type
    funSubsts TyConMap
    tcm ([Type], Type)
    tcSubst [Type]
    args of
      Just Type
    ty -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just Type
    ty
      Maybe Type
    Nothing -> TyConMap -> [([Type], Type)] -> [Type] -> Maybe Type
    findFunSubst TyConMap
    tcm [([Type], Type)]
    rest [Type]
    args

    -- Given a ([LHS match type], RHS type) representing a type function, and
    -- a set of applied types. Match LHS with args, and when successful, return
    -- a substituted RHS
    funSubsts :: TyConMap -> ([Type],Type) -> [Type] -> Maybe Type
    funSubsts :: TyConMap -> ([Type], Type) -> [Type] -> Maybe Type
    funSubsts TyConMap
    tcm ([Type]
    tcSubstLhs,Type
    tcSubstRhs) [Type]
    args = do
      let ([(Type, Type)]
    funArgs,[Type]
    remainder) = [Type] -> [Type] -> ([(Type, Type)], [Type])
    forall {a} {b}. [a] -> [b] -> ([(a, b)], [b])
    zipAtLeast [Type]
    tcSubstLhs [Type]
    args
      [(TyVar, Type)]
    tySubts <- (Maybe [(TyVar, Type)] -> (Type, Type) -> Maybe [(TyVar, Type)])
    -> Maybe [(TyVar, Type)] -> [(Type, Type)] -> Maybe [(TyVar, Type)]
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' (TyConMap
    -> Maybe [(TyVar, Type)] -> (Type, Type) -> Maybe [(TyVar, Type)]
    funSubst TyConMap
    tcm) ([(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just []) [(Type, Type)]
    funArgs
      let tyRhs :: Type
    tyRhs = ([TyVar] -> [Type] -> Type -> Type)
    -> ([TyVar], [Type]) -> Type -> Type
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry HasCallStack => [TyVar] -> [Type] -> Type -> Type
    [TyVar] -> [Type] -> Type -> Type
    substTyWith ([(TyVar, Type)] -> ([TyVar], [Type])
    forall a b. [(a, b)] -> ([a], [b])
    unzip [(TyVar, Type)]
    tySubts) Type
    tcSubstRhs
      -- Type functions can return higher-kinded types
      case [Type]
    remainder of
        []    -> Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Type
    tyRhs
        -- So don't forget to apply the arguments not consumed by the type
        -- function application!
        --
        -- Forgetting leads to: #232
        [Type]
    args' -> Type -> Maybe Type
    forall a. a -> Maybe a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return ((Type -> Type -> Type) -> Type -> [Type] -> Type
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: Type -> Type) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl' Type -> Type -> Type
    AppTy Type
    tyRhs [Type]
    args')
      where
        zipAtLeast :: [a] -> [b] -> ([(a, b)], [b])
    zipAtLeast [] [b]
    ys = ([],[b]
    ys)
        zipAtLeast [a]
    _  [] = String -> ([(a, b)], [b])
    forall a. HasCallStack => String -> a
    error String
    "Under-applied type family"
        zipAtLeast (a
    x:[a]
    xs) (b
    y:[b]
    ys) =
          let ([(a, b)]
    zs,[b]
    remainder) = [a] -> [b] -> ([(a, b)], [b])
    zipAtLeast [a]
    xs [b]
    ys
           in ((a
    x,b
    y)(a, b) -> [(a, b)] -> [(a, b)]
    forall a. a -> [a] -> [a]
    :[(a, b)]
    zs,[b]
    remainder)

    -- Given a LHS matching type, and a RHS to-match type, check if LHS and RHS
    -- are a match. If they do match, and the LHS is a variable, return a
    -- substitution
    funSubst
      :: TyConMap
      -> Maybe [(TyVar,Type)]
      -> (Type,Type)
      -> Maybe [(TyVar,Type)]
    funSubst :: TyConMap
    -> Maybe [(TyVar, Type)] -> (Type, Type) -> Maybe [(TyVar, Type)]
    funSubst TyConMap
    _   Maybe [(TyVar, Type)]
    Nothing  = Maybe [(TyVar, Type)] -> (Type, Type) -> Maybe [(TyVar, Type)]
    forall a b. a -> b -> a
    const Maybe [(TyVar, Type)]
    forall a. Maybe a
    Nothing
    funSubst TyConMap
    tcm (Just [(TyVar, Type)]
    s) = (Type -> Type -> Maybe [(TyVar, Type)])
    -> (Type, Type) -> Maybe [(TyVar, Type)]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Type -> Type -> Maybe [(TyVar, Type)]
    go
      where
        go :: Type -> Type -> Maybe [(TyVar, Type)]
    go (VarTy TyVar
    nmF) Type
    ty = case TyVar -> [(TyVar, Type)] -> Maybe Type
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup TyVar
    nmF [(TyVar, Type)]
    s of
          Maybe Type
    Nothing -> [(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just ((TyVar
    nmF,Type
    ty)(TyVar, Type) -> [(TyVar, Type)] -> [(TyVar, Type)]
    forall a. a -> [a] -> [a]
    :[(TyVar, Type)]
    s)
          -- Given, for example, the type family definition:
          --
          -- > type family Max x y where
          -- >   Max 0 b = b
          -- >   Max a 0 = a
          -- >   Max n n = n
          -- >   Max a b = If (a <=? b) b a
          --
          -- Then `Max 4 8` matches against the 4th clause.
          --
          -- So this is why, whenever we match against a type variable, we first
          -- check if there is already a substitution defined for this type variable,
          -- and if so, the applied type, and the type in the substitution should match.
          Just Type
    ty' | Type
    ty' Type -> Type -> Bool
    `aeqType` Type
    ty -> [(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just [(TyVar, Type)]
    s
          Maybe Type
    _ -> Maybe [(TyVar, Type)]
    forall a. Maybe a
    Nothing

        -- [Note] funSubst FunTy
        --
        -- Whenever type classes have associated types whose instances 'map' to
        -- functions, we try to find substitutions in the LHS and RHS of these
        -- (type-level) functions. Because we use @funSubst@ recursively, we
        -- implicitly check if these functions are of the same arity and match
        -- in the first place. An example of such a construct:
        --
        --   class Example p where
        --     type AB p
        --
        --   instance Example (a -> a) where
        --     type AB (a -> a) = a
        --
        -- In the given example, we would find two substitutions. For example, when
        -- matching against `Char -> Char` we'd find a duplicate `a -> Char`. We
        -- can't think of any (type-checking) cases where these mappings would map
        -- to different types, so this is OK for our purposes.
        go (AppTy Type
    a1 Type
    r1) (AppTy Type
    a2 Type
    r2) = do
          [(TyVar, Type)]
    s1 <- TyConMap
    -> Maybe [(TyVar, Type)] -> (Type, Type) -> Maybe [(TyVar, Type)]
    funSubst TyConMap
    tcm ([(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just [(TyVar, Type)]
    s) (Type
    a1, Type
    a2)
          TyConMap
    -> Maybe [(TyVar, Type)] -> (Type, Type) -> Maybe [(TyVar, Type)]
    funSubst TyConMap
    tcm ([(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just [(TyVar, Type)]
    s1)
                       ( Type
    r1
                       , TyConMap -> Type -> Type
    argView TyConMap
    tcm Type
    r2 -- See [Note: Eager type families]
                       )

        go ty1 :: Type
    ty1@(ConstTy ConstTy
    _) Type
    ty2 =
          -- Looks through AnnType
          if Type
    ty1 Type -> Type -> Bool
    `aeqType` Type
    ty2 then [(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just [(TyVar, Type)]
    s else Maybe [(TyVar, Type)]
    forall a. Maybe a
    Nothing

        go ty1 :: Type
    ty1@(LitTy LitTy
    _) Type
    ty2 =
          -- Looks through AnnType
          if Type
    ty1 Type -> Type -> Bool
    `aeqType` Type
    ty2 then [(TyVar, Type)] -> Maybe [(TyVar, Type)]
    forall a. a -> Maybe a
    Just [(TyVar, Type)]
    s else Maybe [(TyVar, Type)]
    forall a. Maybe a
    Nothing

        go Type
    _ Type
    _ = Maybe [(TyVar, Type)]
    forall a. Maybe a
    Nothing

    {- [Note: Eager type families]

    I don't know whether type families are evaluated strictly or lazily, but since
    type families do not reduce on stuck argument, we assume strictly.
    -}

    reduceTypeFamily :: TyConMap -> Type -> Maybe Type
    reduceTypeFamily :: TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    tcm (Type -> TypeView
    tyView -> TyConApp TyConName
    tc [Type]
    tys)
      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeNatAddTyFamNameKey
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1,Integer
    i2] -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeNatMulTyFamNameKey
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2] -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeNatExpTyFamNameKey
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2] -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^ Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeNatSubTyFamNameKey
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2]
            | let z :: Integer
    z = Integer
    i1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    i2
            , Integer
    z Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0
            -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy Integer
    z))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

    #if !MIN_VERSION_ghc(9,2,0)
      | nameUniq tc == getKey typeNatLeqTyFamNameKey
      = case mapMaybe (litView tcm) tys of
          [i1, i2]
            | Just (FunTyCon {tyConKind = tck}) <- UniqMap.lookup tc tcm
            , (_,tyView -> TyConApp boolTcNm []) <- splitFunTys tcm tck
            , Just boolTc <- UniqMap.lookup boolTcNm tcm
            -> let [falseTc,trueTc] = map (coerce . dcName) (tyConDataCons boolTc)
                in  if i1 <= i2 then Just (mkTyConApp trueTc [])
                                else Just (mkTyConApp falseTc [])
          _ -> Nothing
    #endif

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeNatCmpTyFamNameKey -- "GHC.TypeNats.CmpNat"
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2] ->
            Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ ConstTy -> Type
    ConstTy (ConstTy -> Type) -> ConstTy -> Type
    forall a b. (a -> b) -> a -> b
    $ TyConName -> ConstTy
    TyCon (TyConName -> ConstTy) -> TyConName -> ConstTy
    forall a b. (a -> b) -> a -> b
    $
              case Integer -> Integer -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Integer
    i1 Integer
    i2 of
                Ordering
    LT -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User OccName
    "GHC.Types.LT" (Unique -> Unique
    getKey Unique
    ordLTDataConKey) SrcSpan
    wiredInSrcSpan
                Ordering
    EQ -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User OccName
    "GHC.Types.EQ" (Unique -> Unique
    getKey Unique
    ordEQDataConKey) SrcSpan
    wiredInSrcSpan
                Ordering
    GT -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User OccName
    "GHC.Types.GT" (Unique -> Unique
    getKey Unique
    ordGTDataConKey) SrcSpan
    wiredInSrcSpan
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeSymbolCmpTyFamNameKey -- "GHC.TypeNats.CmpSymbol"
      = case (Type -> Maybe String) -> [Type] -> [String]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe String
    symLitView TyConMap
    tcm) [Type]
    tys of
          [String
    s1, String
    s2] ->
            Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ ConstTy -> Type
    ConstTy (ConstTy -> Type) -> ConstTy -> Type
    forall a b. (a -> b) -> a -> b
    $ TyConName -> ConstTy
    TyCon (TyConName -> ConstTy) -> TyConName -> ConstTy
    forall a b. (a -> b) -> a -> b
    $
              case String -> String -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare String
    s1 String
    s2 of
                Ordering
    LT -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User OccName
    "GHC.Types.LT" (Unique -> Unique
    getKey Unique
    ordLTDataConKey) SrcSpan
    wiredInSrcSpan
                Ordering
    EQ -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User OccName
    "GHC.Types.EQ" (Unique -> Unique
    getKey Unique
    ordEQDataConKey) SrcSpan
    wiredInSrcSpan
                Ordering
    GT -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User OccName
    "GHC.Types.GT" (Unique -> Unique
    getKey Unique
    ordGTDataConKey) SrcSpan
    wiredInSrcSpan
          [String]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

    #if MIN_VERSION_base(4,16,0)
      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeCharCmpTyFamNameKey -- "GHC.TypeNats.CmpSymbol"
      = case (Type -> Maybe Char) -> [Type] -> String
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Char
    charLitView TyConMap
    tcm) [Type]
    tys of
          [Char
    s1, Char
    s2] ->
            Type -> Maybe Type
    forall a. a -> Maybe a
    Just (Type -> Maybe Type) -> Type -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ ConstTy -> Type
    ConstTy (ConstTy -> Type) -> ConstTy -> Type
    forall a b. (a -> b) -> a -> b
    $ TyConName -> ConstTy
    TyCon (TyConName -> ConstTy) -> TyConName -> ConstTy
    forall a b. (a -> b) -> a -> b
    $
              case Char -> Char -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare Char
    s1 Char
    s2 of
                Ordering
    LT -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User (Name -> OccName
    forall a. Show a => a -> OccName
    showt 'LT) (Unique -> Unique
    getKey Unique
    ordLTDataConKey) SrcSpan
    wiredInSrcSpan
                Ordering
    EQ -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User (Name -> OccName
    forall a. Show a => a -> OccName
    showt 'EQ) (Unique -> Unique
    getKey Unique
    ordEQDataConKey) SrcSpan
    wiredInSrcSpan
                Ordering
    GT -> NameSort -> OccName -> Unique -> SrcSpan -> TyConName
    forall a. NameSort -> OccName -> Unique -> SrcSpan -> Name a
    Name NameSort
    User (Name -> OccName
    forall a. Show a => a -> OccName
    showt 'GT) (Unique -> Unique
    getKey Unique
    ordGTDataConKey) SrcSpan
    wiredInSrcSpan
          String
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeConsSymbolTyFamNameKey -- ConsSymbol
      , [Type
    c0, Type
    s0] <- [Type]
    tys
      , Just Char
    c1 <- TyConMap -> Type -> Maybe Char
    charLitView TyConMap
    tcm Type
    c0
      , Just String
    s1 <- TyConMap -> Type -> Maybe String
    symLitView TyConMap
    tcm Type
    s0
      = Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (String -> LitTy
    SymTy (Char
    c1Char -> String -> String
    forall a. a -> [a] -> [a]
    :String
    s1)))

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeUnconsSymbolTyFamNameKey -- UnconsSymbol
      , [String
    s1] <- (Type -> Maybe String) -> [Type] -> [String]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe String
    symLitView TyConMap
    tcm) [Type]
    tys
      = Maybe Type -> Maybe (Maybe Type) -> Maybe Type
    forall a. a -> Maybe a -> a
    fromMaybe (String -> Maybe Type
    forall a. HasCallStack => String -> a
    error String
    "reduceTypeFamily: cannot construct UnconsSymbol result") (Maybe (Maybe Type) -> Maybe Type)
    -> Maybe (Maybe Type) -> Maybe Type
    forall a b. (a -> b) -> a -> b
    $ do
          FunTyCon {tyConKind :: TyCon -> Type
    tyConKind = Type
    tck} <- TyConName -> TyConMap -> Maybe TyCon
    forall a b. Uniquable a => a -> UniqMap b -> Maybe b
    UniqMap.lookup TyConName
    tc TyConMap
    tcm
          TyConApp TyConName
    maybeTcNm [Type
    tupTcApp] <- TypeView -> Maybe TypeView
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Type -> TypeView
    tyView (([Type], Type) -> Type
    forall a b. (a, b) -> b
    snd (TyConMap -> Type -> ([Type], Type)
    splitFunTys TyConMap
    tcm Type
    tck)))
          TyCon
    maybeTc <- TyConName -> TyConMap -> Maybe TyCon
    forall a b. Uniquable a => a -> UniqMap b -> Maybe b
    UniqMap.lookup TyConName
    maybeTcNm TyConMap
    tcm
          [TyConName
    nothingTc,TyConName
    justTc] <- [TyConName] -> Maybe [TyConName]
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ((DataCon -> TyConName) -> [DataCon] -> [TyConName]
    forall a b. (a -> b) -> [a] -> [b]
    map (DcName -> TyConName
    forall a b. Coercible a b => a -> b
    coerce (DcName -> TyConName)
    -> (DataCon -> DcName) -> DataCon -> TyConName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DataCon -> DcName
    dcName) (TyCon -> [DataCon]
    tyConDataCons TyCon
    maybeTc))
          TyConApp TyConName
    tupTcNm [Type
    charTy,Type
    symbolTy] <- TypeView -> Maybe TypeView
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Type -> TypeView
    tyView Type
    tupTcApp)
          TyCon
    tupTc <- TyConName -> TyConMap -> Maybe TyCon
    forall a b. Uniquable a => a -> UniqMap b -> Maybe b
    UniqMap.lookup TyConName
    tupTcNm TyConMap
    tcm
          [TyConName
    tupDc] <- [TyConName] -> Maybe [TyConName]
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure ((DataCon -> TyConName) -> [DataCon] -> [TyConName]
    forall a b. (a -> b) -> [a] -> [b]
    map (DcName -> TyConName
    forall a b. Coercible a b => a -> b
    coerce (DcName -> TyConName)
    -> (DataCon -> DcName) -> DataCon -> TyConName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DataCon -> DcName
    dcName) (TyCon -> [DataCon]
    tyConDataCons TyCon
    tupTc))
          case String
    s1 of
            [] ->
              Maybe Type -> Maybe (Maybe Type)
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Type -> Maybe Type
    forall a. a -> Maybe a
    Just (TyConName -> [Type] -> Type
    mkTyConApp TyConName
    nothingTc [Type
    tupTcApp]))
            (Char
    c:String
    cs) ->
              let tup :: Type
    tup = TyConName -> [Type] -> Type
    mkTyConApp TyConName
    tupDc
                          [Type
    charTy,Type
    symbolTy,LitTy -> Type
    LitTy (Char -> LitTy
    CharTy Char
    c),LitTy -> Type
    LitTy (String -> LitTy
    SymTy String
    cs)]
               in Maybe Type -> Maybe (Maybe Type)
    forall a. a -> Maybe a
    forall (f :: Type -> Type) a. Applicative f => a -> f a
    pure (Type -> Maybe Type
    forall a. a -> Maybe a
    Just (TyConName -> [Type] -> Type
    mkTyConApp TyConName
    justTc [Type
    tupTcApp,Type
    tup]))

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeCharToNatTyFamNameKey -- CharToNat
      , [Char
    c1] <- (Type -> Maybe Char) -> [Type] -> String
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Char
    charLitView TyConMap
    tcm) [Type]
    tys
      = Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Unique -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Char -> Unique
    ord Char
    c1))))

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeNatToCharTyFamNameKey -- NatToChar
      , [Integer
    n1] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys
      = Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Char -> LitTy
    CharTy (Unique -> Char
    chr (Integer -> Unique
    forall a. Num a => Integer -> a
    fromInteger Integer
    n1))))
    #endif

      | TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    tc Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    typeSymbolAppendFamNameKey  -- GHC.TypeLits.AppendSymbol"
      = case (Type -> Maybe String) -> [Type] -> [String]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe String
    symLitView TyConMap
    tcm) [Type]
    tys of
          [String
    s1, String
    s2] ->
            Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (String -> LitTy
    SymTy (String
    s1 String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s2)))
          [String]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.FLog", OccName
    "GHC.TypeNats.FLog"]
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2]
            | Integer
    i1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    1
            , Integer
    i2 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0
            -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Int# -> Integer
    smallInteger (Integer -> Integer -> Int#
    integerLogBase# Integer
    i1 Integer
    i2))))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.CLog", OccName
    "GHC.TypeNats.CLog"]
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2]
            | Just Unique
    k <- Integer -> Integer -> Maybe Unique
    clogBase Integer
    i1 Integer
    i2
            -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Unique -> Integer
    forall a. Integral a => a -> Integer
    toInteger Unique
    k)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.Log", OccName
    "GHC.TypeNats.Log"]
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2]
            | Integer
    i1 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    1
            , Integer
    i2 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0
            -> if Integer
    i2 Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    1
               then Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy Integer
    0))
               else let z1 :: Int#
    z1 = Integer -> Integer -> Int#
    integerLogBase# Integer
    i1 Integer
    i2
                        z2 :: Int#
    z2 = Integer -> Integer -> Int#
    integerLogBase# Integer
    i1 (Integer
    i2Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)
                    in  if Int# -> Bool
    isTrue# (Int#
    z1 Int# -> Int# -> Int#
    ==# Int#
    z2)
                            then Maybe Type
    forall a. Maybe a
    Nothing
                            else Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Int# -> Integer
    smallInteger Int#
    z1)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.GCD", OccName
    "GHC.TypeNats.GCD"]
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2] -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `gcd` Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.LCM", OccName
    "GHC.TypeNats.LCM"]
      = case  (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2] -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `lcm` Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.Div", OccName
    "GHC.TypeNats.Div"]
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2]
            | Integer
    i2 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0
            -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tc OccName -> [OccName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `elem` [OccName
    "GHC.TypeLits.Extra.Mod", OccName
    "GHC.TypeNats.Mod"]
      = case (Type -> Maybe Integer) -> [Type] -> [Integer]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe (TyConMap -> Type -> Maybe Integer
    litView TyConMap
    tcm) [Type]
    tys of
          [Integer
    i1, Integer
    i2]
            | Integer
    i2 Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    0
            -> Type -> Maybe Type
    forall a. a -> Maybe a
    Just (LitTy -> Type
    LitTy (Integer -> LitTy
    NumTy (Integer
    i1 Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    i2)))
          [Integer]
    _ -> Maybe Type
    forall a. Maybe a
    Nothing

      | Just (FunTyCon {tyConSubst :: TyCon -> [([Type], Type)]
    tyConSubst = [([Type], Type)]
    tcSubst}) <- TyConName -> TyConMap -> Maybe TyCon
    forall a b. Uniquable a => a -> UniqMap b -> Maybe b
    UniqMap.lookup TyConName
    tc TyConMap
    tcm
      = let -- See [Note: Eager type families]
            tysR :: [Type]
    tysR = (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map (TyConMap -> Type -> Type
    argView TyConMap
    tcm) [Type]
    tys
         in TyConMap -> [([Type], Type)] -> [Type] -> Maybe Type
    findFunSubst TyConMap
    tcm [([Type], Type)]
    tcSubst [Type]
    tysR

    reduceTypeFamily TyConMap
    _ Type
    _ = Maybe Type
    forall a. Maybe a
    Nothing

    -- |
    isTypeFamilyApplication ::  TyConMap -> Type -> Bool
    isTypeFamilyApplication :: TyConMap -> Type -> Bool
    isTypeFamilyApplication TyConMap
    tcm (Type -> TypeView
    tyView -> TyConApp TyConName
    tcNm [Type]
    _args)
      | Just (FunTyCon {}) <- TyConName -> TyConMap -> Maybe TyCon
    forall a b. Uniquable a => a -> UniqMap b -> Maybe b
    UniqMap.lookup TyConName
    tcNm TyConMap
    tcm = Bool
    True
    isTypeFamilyApplication TyConMap
    _tcm Type
    _type = Bool
    False

    argView :: TyConMap -> Type -> Type
    argView :: TyConMap -> Type -> Type
    argView TyConMap
    m Type
    t = case TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    m Type
    t of
      Maybe Type
    Nothing -> Type
    t
      Just Type
    tR -> TyConMap -> Type -> Type
    argView TyConMap
    m Type
    tR

    litView :: TyConMap -> Type -> Maybe Integer
    litView :: TyConMap -> Type -> Maybe Integer
    litView TyConMap
    _ (LitTy (NumTy Integer
    i))                = Integer -> Maybe Integer
    forall a. a -> Maybe a
    Just Integer
    i
    litView TyConMap
    m (TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    m -> Just Type
    ty') = TyConMap -> Type -> Maybe Integer
    litView TyConMap
    m Type
    ty'
    litView TyConMap
    _ Type
    _ = Maybe Integer
    forall a. Maybe a
    Nothing

    symLitView :: TyConMap -> Type -> Maybe String
    symLitView :: TyConMap -> Type -> Maybe String
    symLitView TyConMap
    _ (LitTy (SymTy String
    s))                = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    s
    symLitView TyConMap
    m (TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    m -> Just Type
    ty') = TyConMap -> Type -> Maybe String
    symLitView TyConMap
    m Type
    ty'
    symLitView TyConMap
    _ Type
    _ = Maybe String
    forall a. Maybe a
    Nothing

    #if MIN_VERSION_base(4,16,0)
    charLitView :: TyConMap -> Type -> Maybe Char
    charLitView :: TyConMap -> Type -> Maybe Char
    charLitView TyConMap
    _ (LitTy (CharTy Char
    c)) = Char -> Maybe Char
    forall a. a -> Maybe a
    Just Char
    c
    charLitView TyConMap
    m (TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    m -> Just Type
    t) = TyConMap -> Type -> Maybe Char
    charLitView TyConMap
    m Type
    t
    charLitView TyConMap
    _ Type
    _ = Maybe Char
    forall a. Maybe a
    Nothing
    #endif

    isIntegerTy :: Type -> Bool
    isIntegerTy :: Type -> Bool
    isIntegerTy (ConstTy (TyCon TyConName
    nm)) = TyConName -> Unique
    forall a. Name a -> Unique
    nameUniq TyConName
    nm Unique -> Unique -> Bool
    forall a. Eq a => a -> a -> Bool
    == Unique -> Unique
    getKey Unique
    integerTyConKey
    isIntegerTy Type
    _ = Bool
    False

    -- | Normalize a type, looking through Signals and newtypes
    --
    -- For example: @Signal a (Vec (6-1) (Unsigned (3+1)))@ normalizes to @Vec 5 (Unsigned 4)@
    normalizeType :: TyConMap -> Type -> Type
    normalizeType :: TyConMap -> Type -> Type
    normalizeType TyConMap
    tcMap = Type -> Type
    go
      where
      go :: Type -> Type
    go Type
    ty = case Type -> TypeView
    tyView Type
    ty of
        TyConApp TyConName
    tcNm [Type]
    args
          -- These Clash types are implemented with newtypes.
          -- We need to keep these newtypes because they define the width of the numbers.
          | TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Sized.Internal.BitVector.Bit" Bool -> Bool -> Bool
    ||
            TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Sized.Internal.BitVector.BitVector" Bool -> Bool -> Bool
    ||
            TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Sized.Internal.Index.Index"         Bool -> Bool -> Bool
    ||
            TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Sized.Internal.Signed.Signed"       Bool -> Bool -> Bool
    ||
            TyConName -> OccName
    forall a. Name a -> OccName
    nameOcc TyConName
    tcNm OccName -> OccName -> Bool
    forall a. Eq a => a -> a -> Bool
    == OccName
    "Clash.Sized.Internal.Unsigned.Unsigned"
          -> TyConName -> [Type] -> Type
    mkTyConApp TyConName
    tcNm ((Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    go [Type]
    args)
          | Bool
    otherwise
          -> case TyConName -> TyConMap -> TyCon
    forall a b. Uniquable a => a -> UniqMap b -> b
    UniqMap.find TyConName
    tcNm TyConMap
    tcMap of
              AlgTyCon {algTcRhs :: TyCon -> AlgTyConRhs
    algTcRhs = (NewTyCon DataCon
    _ ([TyVar], Type)
    nt)}
                 -> case ([TyVar], Type) -> [Type] -> Maybe Type
    newTyConInstRhs ([TyVar], Type)
    nt [Type]
    args of
                      Just Type
    ty' -> Type -> Type
    go Type
    ty'
                      Maybe Type
    Nothing  -> Type
    ty
              TyCon
    _ ->
                 let args' :: [Type]
    args' = (Type -> Type) -> [Type] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Type -> Type
    go [Type]
    args
                     ty' :: Type
    ty' = TyConName -> [Type] -> Type
    mkTyConApp TyConName
    tcNm [Type]
    args'
                 in case TyConMap -> Type -> Maybe Type
    reduceTypeFamily TyConMap
    tcMap Type
    ty' of
                   -- TODO Instead of recursing here, reduceTypeFamily should
                   -- ensure that if the result is a reducible type family it is
                   -- also reduced. This would reduce traversals over a type.
                   --
                   -- It may be a good idea to keep reduceTypeFamily only reducing
                   -- one family, and definiing reduceTypeFamilies to reduce all
                   -- it encounters in one traversal.
                   Just Type
    ty'' -> Type -> Type
    go Type
    ty''
                   Maybe Type
    Nothing  -> Type
    ty'
        FunTy Type
    ty1 Type
    ty2 -> Type -> Type -> Type
    mkFunTy (Type -> Type
    go Type
    ty1) (Type -> Type
    go Type
    ty2)
        OtherType (ForAllTy TyVar
    tyvar Type
    ty')
          -> TyVar -> Type -> Type
    ForAllTy TyVar
    tyvar (Type -> Type
    go Type
    ty')
        TypeView
    _ -> Type
    ty

    isClassTy
      :: TyConMap
      -> Type
      -> Bool
    isClassTy :: TyConMap -> Type -> Bool
    isClassTy TyConMap
    tcm (Type -> TypeView
    tyView -> TyConApp TyConName
    tcNm [Type]
    _) =
      case TyConName -> TyConMap -> Maybe TyCon
    forall a b. Uniquable a => a -> UniqMap b -> Maybe b
    UniqMap.lookup TyConName
    tcNm TyConMap
    tcm of
        Just (AlgTyCon {Bool
    isClassTc :: Bool
    isClassTc :: TyCon -> Bool
    isClassTc}) -> Bool
    isClassTc
        Maybe TyCon
    _ -> Bool
    False
    isClassTy TyConMap
    _ Type
    _ = Bool
    False