{-|
  Copyright   :  (C) 2012-2016, University of Twente,
                     2016     , Myrtle Software Ltd,
                     2017     , Google Inc.
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  Christiaan Baaij <christiaan.baaij@gmail.com>

  Types in CoreHW
-}

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

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

-- External import
import           Control.DeepSeq        as DS
import           Data.Binary            (Binary)
import           Data.Coerce            (coerce)
import           Data.Hashable          (Hashable)
import           Data.List              (foldl')
import           Data.List.Extra        (splitAtList)
import           Data.Maybe             (isJust, mapMaybe)
import           GHC.Base               (isTrue#,(==#))
import           GHC.Generics           (Generic(..))
import           GHC.Integer            (smallInteger)
import           GHC.Integer.Logarithms (integerLogBase#)

-- GHC API
#if MIN_VERSION_ghc(9,0,0)
import           GHC.Builtin.Names
  (integerTyConKey, typeNatAddTyFamNameKey, typeNatExpTyFamNameKey,
   typeNatLeqTyFamNameKey, 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.Core.DataCon
import           Clash.Core.Name
import {-# SOURCE #-} Clash.Core.Subst
import           Clash.Core.TyCon
import           Clash.Core.TysPrim
import           Clash.Core.Var
import           Clash.Unique
import           Clash.Util

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

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

varAttrs (Id Name a
_ Unique
_ Type
ty IdScope
_) =
  case Type
ty of
    AnnType [Attr']
attrs Type
_typ -> [Attr']
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'] !Type      -- ^ Annotated type, see Clash.Annotations.SynthesisAttributes
  deriving (Unique -> Type -> [Char] -> [Char]
[Type] -> [Char] -> [Char]
Type -> [Char]
(Unique -> Type -> [Char] -> [Char])
-> (Type -> [Char]) -> ([Type] -> [Char] -> [Char]) -> Show Type
forall a.
(Unique -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [Type] -> [Char] -> [Char]
$cshowList :: [Type] -> [Char] -> [Char]
show :: Type -> [Char]
$cshow :: Type -> [Char]
showsPrec :: Unique -> Type -> [Char] -> [Char]
$cshowsPrec :: Unique -> Type -> [Char] -> [Char]
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
$cto :: forall x. Rep Type x -> Type
$cfrom :: forall x. Type -> Rep Type x
Generic,Type -> ()
(Type -> ()) -> NFData Type
forall a. (a -> ()) -> NFData a
rnf :: Type -> ()
$crnf :: Type -> ()
NFData,Unique -> Type -> Unique
Type -> Unique
(Unique -> Type -> Unique) -> (Type -> Unique) -> Hashable Type
forall a. (Unique -> a -> Unique) -> (a -> Unique) -> Hashable a
hash :: Type -> Unique
$chash :: Type -> Unique
hashWithSalt :: Unique -> Type -> Unique
$chashWithSalt :: Unique -> Type -> Unique
Hashable,Get Type
[Type] -> Put
Type -> Put
(Type -> Put) -> Get Type -> ([Type] -> Put) -> Binary Type
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
putList :: [Type] -> Put
$cputList :: [Type] -> Put
get :: Get Type
$cget :: Get Type
put :: Type -> Put
$cput :: Type -> Put
Binary)

-- | 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 -> [Char] -> [Char]
[TypeView] -> [Char] -> [Char]
TypeView -> [Char]
(Unique -> TypeView -> [Char] -> [Char])
-> (TypeView -> [Char])
-> ([TypeView] -> [Char] -> [Char])
-> Show TypeView
forall a.
(Unique -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [TypeView] -> [Char] -> [Char]
$cshowList :: [TypeView] -> [Char] -> [Char]
show :: TypeView -> [Char]
$cshow :: TypeView -> [Char]
showsPrec :: Unique -> TypeView -> [Char] -> [Char]
$cshowsPrec :: Unique -> TypeView -> [Char] -> [Char]
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
/= :: ConstTy -> ConstTy -> Bool
$c/= :: ConstTy -> ConstTy -> Bool
== :: ConstTy -> ConstTy -> Bool
$c== :: 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
min :: ConstTy -> ConstTy -> ConstTy
$cmin :: ConstTy -> ConstTy -> ConstTy
max :: ConstTy -> ConstTy -> ConstTy
$cmax :: ConstTy -> ConstTy -> ConstTy
>= :: ConstTy -> ConstTy -> Bool
$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
compare :: ConstTy -> ConstTy -> Ordering
$ccompare :: ConstTy -> ConstTy -> Ordering
$cp1Ord :: Eq ConstTy
Ord,Unique -> ConstTy -> [Char] -> [Char]
[ConstTy] -> [Char] -> [Char]
ConstTy -> [Char]
(Unique -> ConstTy -> [Char] -> [Char])
-> (ConstTy -> [Char])
-> ([ConstTy] -> [Char] -> [Char])
-> Show ConstTy
forall a.
(Unique -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [ConstTy] -> [Char] -> [Char]
$cshowList :: [ConstTy] -> [Char] -> [Char]
show :: ConstTy -> [Char]
$cshow :: ConstTy -> [Char]
showsPrec :: Unique -> ConstTy -> [Char] -> [Char]
$cshowsPrec :: Unique -> ConstTy -> [Char] -> [Char]
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
$cto :: forall x. Rep ConstTy x -> ConstTy
$cfrom :: forall x. ConstTy -> Rep ConstTy x
Generic,ConstTy -> ()
(ConstTy -> ()) -> NFData ConstTy
forall a. (a -> ()) -> NFData a
rnf :: ConstTy -> ()
$crnf :: ConstTy -> ()
NFData,Unique -> ConstTy -> Unique
ConstTy -> Unique
(Unique -> ConstTy -> Unique)
-> (ConstTy -> Unique) -> Hashable ConstTy
forall a. (Unique -> a -> Unique) -> (a -> Unique) -> Hashable a
hash :: ConstTy -> Unique
$chash :: ConstTy -> Unique
hashWithSalt :: Unique -> ConstTy -> Unique
$chashWithSalt :: Unique -> 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
putList :: [ConstTy] -> Put
$cputList :: [ConstTy] -> Put
get :: Get ConstTy
$cget :: Get ConstTy
put :: ConstTy -> Put
$cput :: ConstTy -> Put
Binary)

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

-- | 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 TyConMap
tcMap TyConMap -> TyConName -> TyCon
forall a b. (HasCallStack, Uniquable a) => UniqMap b -> a -> b
`lookupUniqMap'` TyConName
tcNm 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
  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 (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 (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 (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 (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 a Superkind?
isSuperKind :: TyConMap -> Type -> Bool
isSuperKind :: TyConMap -> Type -> Bool
isSuperKind TyConMap
tcMap (ConstTy (TyCon ((TyConMap
tcMap TyConMap -> TyConName -> TyCon
forall a b. (HasCallStack, Uniquable a) => UniqMap b -> a -> b
`lookupUniqMap'`) -> SuperKindTyCon {}))) = Bool
True
isSuperKind TyConMap
_ Type
_ = Bool
False

-- | Determine the kind of a type
typeKind :: TyConMap -> Type -> Kind
typeKind :: TyConMap -> Type -> Type
typeKind TyConMap
_ (VarTy TyVar
k)            = TyVar -> Type
forall a. Var a -> Type
varType TyVar
k
typeKind TyConMap
m (ForAllTy TyVar
_ Type
ty)      = TyConMap -> Type -> Type
typeKind TyConMap
m Type
ty
typeKind TyConMap
_ (LitTy (NumTy Integer
_))    = Type
typeNatKind
typeKind TyConMap
_ (LitTy (SymTy [Char]
_))    = Type
typeSymbolKind
typeKind TyConMap
m (AnnType [Attr']
_ann Type
typ)   = TyConMap -> Type -> Type
typeKind TyConMap
m Type
typ
typeKind TyConMap
m (Type -> TypeView
tyView -> FunTy Type
_arg Type
res)
  | TyConMap -> Type -> Bool
isSuperKind TyConMap
m Type
k = Type
k
  | Bool
otherwise       = Type
liftedTypeKind
  where k :: Type
k = TyConMap -> Type -> Type
typeKind TyConMap
m Type
res

typeKind TyConMap
m (Type -> TypeView
tyView -> TyConApp TyConName
tc [Type]
args) =
  (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type -> Type -> Type
kindFunResult (TyCon -> Type
tyConKind (TyConMap
m TyConMap -> TyConName -> TyCon
forall a b. (HasCallStack, Uniquable a) => UniqMap b -> a -> b
`lookupUniqMap'` TyConName
tc)) [Type]
args

typeKind TyConMap
m (AppTy Type
fun Type
arg)      = Type -> Type -> Type
kindFunResult (TyConMap -> Type -> Type
typeKind TyConMap
m Type
fun) Type
arg
typeKind TyConMap
_ (ConstTy ConstTy
ct)         = [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"typeKind: naked ConstTy: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ConstTy -> [Char]
forall a. Show a => a -> [Char]
show ConstTy
ct

kindFunResult :: Kind -> KindOrType -> Kind
kindFunResult :: Type -> Type -> Type
kindFunResult (Type -> TypeView
tyView -> FunTy Type
_ Type
res) Type
_ = Type
res

kindFunResult (ForAllTy TyVar
kv Type
ki) Type
arg =
  HasCallStack => [TyVar] -> [Type] -> Type -> Type
[TyVar] -> [Type] -> Type -> Type
substTyWith [TyVar
kv] [Type
arg] Type
ki

kindFunResult Type
k Type
tys =
  [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"kindFunResult: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Type, Type) -> [Char]
forall a. Show a => a -> [Char]
show (Type
k,Type
tys)

-- | 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 (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 (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']
typeAttrs :: Type -> [Attr']
typeAttrs (AnnType [Attr']
attrs Type
_typ) = [Attr']
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
_ = [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"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 (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 (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 (m :: Type -> Type) a. Monad m => a -> m a
return ((Type -> Type -> Type) -> Type -> [Type] -> Type
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]
_  [] = [Char] -> ([(a, b)], [b])
forall a. HasCallStack => [Char] -> a
error [Char]
"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

  | TyConName -> Unique
forall a. Name a -> Unique
nameUniq TyConName
tc Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Unique
getKey Unique
typeNatLeqTyFamNameKey
  = 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 (FunTyCon {tyConKind :: TyCon -> Type
tyConKind = Type
tck}) <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
tc TyConMap
tcm
        , ([Type]
_,Type -> TypeView
tyView -> TyConApp TyConName
boolTcNm []) <- TyConMap -> Type -> ([Type], Type)
splitFunTys TyConMap
tcm Type
tck
        , Just TyCon
boolTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
boolTcNm TyConMap
tcm
        -> let [TyConName
falseTc,TyConName
trueTc] = (DataCon -> TyConName) -> [DataCon] -> [TyConName]
forall a b. (a -> b) -> [a] -> [b]
map (DcName -> TyConName
coerce (DcName -> TyConName)
-> (DataCon -> DcName) -> DataCon -> TyConName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> DcName
dcName) (TyCon -> [DataCon]
tyConDataCons TyCon
boolTc)
            in  if Integer
i1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
i2 then Type -> Maybe Type
forall a. a -> Maybe a
Just (TyConName -> [Type] -> Type
mkTyConApp TyConName
trueTc [])
                            else Type -> Maybe Type
forall a. a -> Maybe a
Just (TyConName -> [Type] -> Type
mkTyConApp TyConName
falseTc [])
      [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
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 [Char]) -> [Type] -> [[Char]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe [Char]
symLitView 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 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
      [[Char]]
_ -> 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
typeSymbolAppendFamNameKey  -- GHC.TypeLits.AppendSymbol"
  = case (Type -> Maybe [Char]) -> [Type] -> [[Char]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe [Char]
symLitView TyConMap
tcm) [Type]
tys of
      [[Char]
s1, [Char]
s2] ->
        Type -> Maybe Type
forall a. a -> Maybe a
Just (LitTy -> Type
LitTy ([Char] -> LitTy
SymTy ([Char]
s1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s2)))
      [[Char]]
_ -> Maybe Type
forall a. Maybe a
Nothing

  | TyConName -> OccName
forall a. Name a -> OccName
nameOcc TyConName
tc OccName -> [OccName] -> 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 (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 (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 (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 (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 (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 (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
lookupUniqMap 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
lookupUniqMap 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 [Char]
symLitView TyConMap
_ (LitTy (SymTy [Char]
s))                = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
symLitView TyConMap
m (TyConMap -> Type -> Maybe Type
reduceTypeFamily TyConMap
m -> Just Type
ty') = TyConMap -> Type -> Maybe [Char]
symLitView TyConMap
m Type
ty'
symLitView TyConMap
_ Type
_ = Maybe [Char]
forall a. Maybe a
Nothing

-- | The type @forall a . a@
undefinedTy ::Type
undefinedTy :: Type
undefinedTy =
  let aNm :: Name a
aNm = OccName -> Unique -> Name a
forall a. OccName -> Unique -> Name a
mkUnsafeSystemName OccName
"a" Unique
0
      aTv :: Var a
aTv = (Name a -> Unique -> Type -> Var a
forall a. Name a -> Unique -> Type -> Var a
TyVar Name a
forall a. Name a
aNm Unique
0 Type
liftedTypeKind)
  in  TyVar -> Type -> Type
ForAllTy TyVar
forall a. Var a
aTv (TyVar -> Type
VarTy TyVar
forall a. Var a
aTv)

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 TyConMap -> TyConName -> TyCon
forall a b. (HasCallStack, Uniquable a) => UniqMap b -> a -> b
lookupUniqMap' TyConMap
tcMap TyConName
tcNm 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
lookupUniqMap TyConName
tcNm TyConMap
tcm of
    Just (AlgTyCon {Bool
isClassTc :: TyCon -> Bool
isClassTc :: Bool
isClassTc}) -> Bool
isClassTc
    Maybe TyCon
_ -> Bool
False
isClassTy TyConMap
_ Type
_ = Bool
False