{-|
  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.Maybe             (isJust, mapMaybe)
import           GHC.Base               (isTrue#,(==#))
import           GHC.Generics           (Generic(..))
import           GHC.Integer            (smallInteger)
import           GHC.Integer.Logarithms (integerLogBase#)

-- GHC API
#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)

-- 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
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "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 _ _ ty :: Type
ty _) =
  case Type
ty of
    AnnType attrs :: [Attr']
attrs _typ :: Type
_typ -> [Attr']
attrs
    _                  -> []


-- | 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 (Int -> Type -> [Char] -> [Char]
[Type] -> [Char] -> [Char]
Type -> [Char]
(Int -> Type -> [Char] -> [Char])
-> (Type -> [Char]) -> ([Type] -> [Char] -> [Char]) -> Show Type
forall a.
(Int -> 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 :: Int -> Type -> [Char] -> [Char]
$cshowsPrec :: Int -> 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,Int -> Type -> Int
Type -> Int
(Int -> Type -> Int) -> (Type -> Int) -> Hashable Type
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Type -> Int
$chash :: Type -> Int
hashWithSalt :: Int -> Type -> Int
$chashWithSalt :: Int -> Type -> Int
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 Int -> TypeView -> [Char] -> [Char]
[TypeView] -> [Char] -> [Char]
TypeView -> [Char]
(Int -> TypeView -> [Char] -> [Char])
-> (TypeView -> [Char])
-> ([TypeView] -> [Char] -> [Char])
-> Show TypeView
forall a.
(Int -> 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 :: Int -> TypeView -> [Char] -> [Char]
$cshowsPrec :: Int -> 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,Int -> ConstTy -> [Char] -> [Char]
[ConstTy] -> [Char] -> [Char]
ConstTy -> [Char]
(Int -> ConstTy -> [Char] -> [Char])
-> (ConstTy -> [Char])
-> ([ConstTy] -> [Char] -> [Char])
-> Show ConstTy
forall a.
(Int -> 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 :: Int -> ConstTy -> [Char] -> [Char]
$cshowsPrec :: Int -> 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,Int -> ConstTy -> Int
ConstTy -> Int
(Int -> ConstTy -> Int) -> (ConstTy -> Int) -> Hashable ConstTy
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: ConstTy -> Int
$chash :: ConstTy -> Int
hashWithSalt :: Int -> ConstTy -> Int
$chashWithSalt :: Int -> ConstTy -> Int
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,Int -> LitTy -> [Char] -> [Char]
[LitTy] -> [Char] -> [Char]
LitTy -> [Char]
(Int -> LitTy -> [Char] -> [Char])
-> (LitTy -> [Char]) -> ([LitTy] -> [Char] -> [Char]) -> Show LitTy
forall a.
(Int -> 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 :: Int -> LitTy -> [Char] -> [Char]
$cshowsPrec :: Int -> 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,Int -> LitTy -> Int
LitTy -> Int
(Int -> LitTy -> Int) -> (LitTy -> Int) -> Hashable LitTy
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: LitTy -> Int
$chash :: LitTy -> Int
hashWithSalt :: Int -> LitTy -> Int
$chashWithSalt :: Int -> LitTy -> Int
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 tOrig :: Type
tOrig = case Type
tOrig of
  ConstTy c :: ConstTy
c -> case ConstTy
c of
    TyCon tc :: TyConName
tc -> TyConName -> [Type] -> TypeView
TyConApp TyConName
tc []
    _ -> Type -> TypeView
OtherType Type
tOrig
  AppTy l0 :: Type
l0 res :: Type
res -> case Type
l0 of
    ConstTy (TyCon tc :: TyConName
tc) -> TyConName -> [Type] -> TypeView
TyConApp TyConName
tc [Type
res]
    AppTy l1 :: Type
l1 arg :: Type
arg -> case Type
l1 of
      ConstTy Arrow -> Type -> Type -> TypeView
FunTy Type
arg Type
res
      ConstTy (TyCon tc :: TyConName
tc) -> TyConName -> [Type] -> TypeView
TyConApp TyConName
tc [Type
arg,Type
res]
      AppTy l2 :: Type
l2 resK :: Type
resK -> case Type
l2 of
        ConstTy (TyCon tc :: TyConName
tc) -> TyConName -> [Type] -> TypeView
TyConApp TyConName
tc [Type
resK,Type
arg,Type
res]
        AppTy l3 :: Type
l3 argK :: Type
argK -> case Type
l3 of
          ConstTy (TyCon tc :: TyConName
tc) -> TyConName -> [Type] -> TypeView
TyConApp TyConName
tc [Type
argK,Type
resK,Type
arg,Type
res]
          ConstTy Arrow -> Type -> Type -> TypeView
FunTy Type
arg Type
res -- See Note [Arrow arguments]
          _ -> case [Type] -> Type -> (Type, [Type])
go [Type
argK,Type
resK,Type
arg,Type
res] Type
l3 of
            (ConstTy (TyCon tc :: TyConName
tc),args :: [Type]
args)
              -> TyConName -> [Type] -> TypeView
TyConApp TyConName
tc [Type]
args
            _ -> Type -> TypeView
OtherType Type
tOrig
        _ -> Type -> TypeView
OtherType Type
tOrig
      _ -> Type -> TypeView
OtherType Type
tOrig
    _ -> Type -> TypeView
OtherType Type
tOrig
  _ -> Type -> TypeView
OtherType Type
tOrig
 where
  go :: [Type] -> Type -> (Type, [Type])
go args :: [Type]
args (AppTy ty1 :: Type
ty1 ty2 :: Type
ty2) = [Type] -> Type -> (Type, [Type])
go (Type
ty2Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
ty1
  go args :: [Type]
args t1 :: 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 tcm :: TyConMap
tcm ty :: Type
ty =
  case TyConMap -> Type -> Maybe Type
coreView1 TyConMap
tcm Type
ty of
    Nothing  -> Type
ty
    Just ty' :: 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 tcMap :: TyConMap
tcMap ty :: Type
ty = case Type -> TypeView
tyView Type
ty of
  TyConApp tcNm :: TyConName
tcNm args :: [Type]
args
    | TyConName -> OccName
forall a. Name a -> OccName
nameOcc TyConName
tcNm OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== "Clash.Signal.BiSignal.BiSignalIn"
    , [_,_,_,elTy :: 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
== "Clash.Signal.BiSignal.BiSignalOut"
    , [_,_,_,elTy :: 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
== "Clash.Signal.Internal.Signal"
    , [_,elTy :: 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 _ nt :: ([TyVar], Type)
nt)}
           -> ([TyVar], Type) -> [Type] -> Maybe Type
newTyConInstRhs ([TyVar], Type)
nt [Type]
args
         _ -> TyConMap -> Type -> Maybe Type
reduceTypeFamily TyConMap
tcMap Type
ty
  _ -> 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 (tvs :: [TyVar]
tvs,ty :: Type
ty) tys :: [Type]
tys
    | [TyVar] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [TyVar]
tvs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
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
    (tys1 :: [Type]
tys1, tys2 :: [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 t1 :: 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 tc :: 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 ty :: 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 tc :: TyConName
tc args :: [Type]
args) = (TyConName, [Type]) -> Maybe (TyConName, [Type])
forall a. a -> Maybe a
Just (TyConName
tc,[Type]
args)
splitTyConAppM _                            = Maybe (TyConName, [Type])
forall a. Maybe a
Nothing

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

-- | Determine the kind of a type
typeKind :: TyConMap -> Type -> Kind
typeKind :: TyConMap -> Type -> Type
typeKind _ (VarTy k :: TyVar
k)            = TyVar -> Type
forall a. Var a -> Type
varType TyVar
k
typeKind m :: TyConMap
m (ForAllTy _ ty :: Type
ty)      = TyConMap -> Type -> Type
typeKind TyConMap
m Type
ty
typeKind _ (LitTy (NumTy _))    = Type
typeNatKind
typeKind _ (LitTy (SymTy _))    = Type
typeSymbolKind
typeKind m :: TyConMap
m (AnnType _ann :: [Attr']
_ann typ :: Type
typ)   = TyConMap -> Type -> Type
typeKind TyConMap
m Type
typ
typeKind m :: TyConMap
m (Type -> TypeView
tyView -> FunTy _arg :: Type
_arg res :: 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 m :: TyConMap
m (Type -> TypeView
tyView -> TyConApp tc :: TyConName
tc args :: [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 m :: TyConMap
m (AppTy fun :: Type
fun arg :: Type
arg)      = Type -> Type -> Type
kindFunResult (TyConMap -> Type -> Type
typeKind TyConMap
m Type
fun) Type
arg
typeKind _ (ConstTy ct :: ConstTy
ct)         = [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "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 _ res :: Type
res) _ = Type
res

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

kindFunResult k :: Type
k tys :: Type
tys =
  [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "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 _ _)          = Bool
True
isPolyTy (Type -> TypeView
tyView -> FunTy _ res :: Type
res) = Type -> Bool
isPolyTy Type
res
isPolyTy _                       = 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 m :: TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just ty :: Type
ty)  = TyConMap -> Type -> Maybe (Type, Type)
splitFunTy TyConMap
m Type
ty
splitFunTy _ (Type -> TypeView
tyView -> FunTy arg :: Type
arg res :: Type
res) = (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
arg,Type
res)
splitFunTy _ _ = Maybe (Type, Type)
forall a. Maybe a
Nothing

splitFunTys :: TyConMap
            -> Type
            -> ([Type],Type)
splitFunTys :: TyConMap -> Type -> ([Type], Type)
splitFunTys m :: TyConMap
m ty :: Type
ty = [Type] -> Type -> Type -> ([Type], Type)
go [] Type
ty Type
ty
  where
    go :: [Type] -> Type -> Type -> ([Type], Type)
go args :: [Type]
args orig_ty :: Type
orig_ty (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just ty' :: Type
ty') = [Type] -> Type -> Type -> ([Type], Type)
go [Type]
args Type
orig_ty Type
ty'
    go args :: [Type]
args _       (Type -> TypeView
tyView -> FunTy arg :: Type
arg res :: Type
res) = [Type] -> Type -> Type -> ([Type], Type)
go (Type
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args) Type
res Type
res
    go args :: [Type]
args orig_ty :: Type
orig_ty _                         = ([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 args :: [Either TyVar Type]
args (ForAllTy tv :: TyVar
tv ty :: 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 args :: [Either TyVar Type]
args (Type -> TypeView
tyView -> FunTy arg :: Type
arg res :: 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 args :: [Either TyVar Type]
args ty :: 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 tcm :: TyConMap
tcm ty :: 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 args :: [Either TyVar Type]
args orig_ty :: Type
orig_ty (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
tcm -> Just ty' :: Type
ty') = [Either TyVar Type] -> Type -> Type -> ([Either TyVar Type], Type)
go [Either TyVar Type]
args Type
orig_ty Type
ty'
    go args :: [Either TyVar Type]
args _       (ForAllTy tv :: TyVar
tv res :: 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 args :: [Either TyVar Type]
args _       (Type -> TypeView
tyView -> FunTy arg :: Type
arg res :: 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 args :: [Either TyVar Type]
args orig_ty :: Type
orig_ty _                           = ([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 m :: TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just ty :: Type
ty) = TyConMap -> Type -> Bool
isPolyFunCoreTy TyConMap
m Type
ty
isPolyFunCoreTy _ ty :: Type
ty = case Type -> TypeView
tyView Type
ty of
  FunTy _ _ -> Bool
True
  OtherType (ForAllTy _ _) -> Bool
True
  _ -> 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 attrs :: [Attr']
attrs _typ :: Type
_typ) = [Attr']
attrs
typeAttrs _                    = []

-- | Is a type a function type?
isFunTy :: TyConMap
        -> Type
        -> Bool
isFunTy :: TyConMap -> Type -> Bool
isFunTy m :: 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 m :: TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just ty :: Type
ty)   arg :: Type
arg = TyConMap -> Type -> Type -> Type
applyFunTy TyConMap
m Type
ty Type
arg
applyFunTy _ (Type -> TypeView
tyView -> FunTy _ resTy :: Type
resTy) _    = Type
resTy
applyFunTy _ _ _ = [Char] -> Type
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ $(curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ "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 _   [] _ = Maybe Type
forall a. Maybe a
Nothing
findFunSubst tcm :: TyConMap
tcm (tcSubst :: ([Type], Type)
tcSubst:rest :: [([Type], Type)]
rest) args :: [Type]
args = case TyConMap -> ([Type], Type) -> [Type] -> Maybe Type
funSubsts TyConMap
tcm ([Type], Type)
tcSubst [Type]
args of
  Just ty :: Type
ty -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
  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 tcm :: TyConMap
tcm (tcSubstLhs :: [Type]
tcSubstLhs,tcSubstRhs :: Type
tcSubstRhs) args :: [Type]
args = do
  [(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] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
tcSubstLhs [Type]
args)
  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 Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop ([Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Type]
tcSubstLhs) [Type]
args 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
    args' :: [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')

-- 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 _   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 tcm :: TyConMap
tcm (Just s :: [(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 nmF :: TyVar
nmF) ty :: 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
      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 ty' :: 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 [(TyVar, Type)]
forall a. Maybe a
Nothing
    go ty1 :: Type
ty1 (TyConMap -> Type -> Maybe Type
reduceTypeFamily TyConMap
tcm -> Just ty2 :: Type
ty2) = Type -> Type -> Maybe [(TyVar, Type)]
go Type
ty1 Type
ty2 -- See [Note: lazy type families]
    go ty1 :: Type
ty1@(LitTy _) ty2 :: Type
ty2 = 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 -> TypeView
tyView -> TyConApp tc :: TyConName
tc argTys :: [Type]
argTys) (Type -> TypeView
tyView -> TyConApp tc' :: TyConName
tc' argTys' :: [Type]
argTys')
      | TyConName
tc TyConName -> TyConName -> Bool
forall a. Eq a => a -> a -> Bool
== TyConName
tc'
      = (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 [(TyVar, Type)]
s) ([Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
argTys [Type]
argTys')
    -- 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 (Type -> TypeView
tyView -> FunTy a :: Type
a b :: Type
b) (Type -> TypeView
tyView -> FunTy a' :: Type
a' b' :: Type
b') =
      [(TyVar, Type)] -> [(TyVar, Type)] -> [(TyVar, Type)]
forall a. [a] -> [a] -> [a]
(++) ([(TyVar, Type)] -> [(TyVar, Type)] -> [(TyVar, Type)])
-> Maybe [(TyVar, Type)]
-> Maybe ([(TyVar, Type)] -> [(TyVar, Type)])
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
a, Type
a')
           Maybe ([(TyVar, Type)] -> [(TyVar, Type)])
-> Maybe [(TyVar, Type)] -> Maybe [(TyVar, Type)]
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> 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
b, Type
b')

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

{- [Note: lazy type families]

I don't know whether type families are evaluated strictly or lazily, but this
being Haskell, I assume type families are evaluated lazily.

Clash hence follows the Haskell way, and only evaluates type family arguments
to (WH)NF when the formal parameter is _not_ a type variable.
-}

reduceTypeFamily :: TyConMap -> Type -> Maybe Type
reduceTypeFamily :: TyConMap -> Type -> Maybe Type
reduceTypeFamily tcm :: TyConMap
tcm (Type -> TypeView
tyView -> TyConApp tc :: TyConName
tc tys :: [Type]
tys)
  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeNatAddTyFamNameKey
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (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 (Integer -> LitTy
NumTy (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i2)))

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeNatMulTyFamNameKey
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (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 (Integer -> LitTy
NumTy (Integer
i1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
i2)))

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeNatExpTyFamNameKey
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (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 (Integer -> LitTy
NumTy (Integer
i1 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
i2)))

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeNatSubTyFamNameKey
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , 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
>= 0
  = Type -> Maybe Type
forall a. a -> Maybe a
Just (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
z))

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeNatLeqTyFamNameKey
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , 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 -> TypeView
tyView -> TyConApp boolTcNm :: TyConName
boolTcNm []) <- TyConMap -> Type -> ([Type], Type)
splitFunTys TyConMap
tcm Type
tck
  , Just boolTc :: TyCon
boolTc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
boolTcNm TyConMap
tcm
  = let [falseTc :: TyConName
falseTc,trueTc :: TyConName
trueTc] = (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
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 [])

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeNatCmpTyFamNameKey -- "GHC.TypeNats.CmpNat"
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (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 (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
        LT -> NameSort -> OccName -> Int -> SrcSpan -> TyConName
forall a. NameSort -> OccName -> Int -> SrcSpan -> Name a
Name NameSort
User "GHC.Types.LT" (Unique -> Int
getKey Unique
ordLTDataConKey) SrcSpan
wiredInSrcSpan
        EQ -> NameSort -> OccName -> Int -> SrcSpan -> TyConName
forall a. NameSort -> OccName -> Int -> SrcSpan -> Name a
Name NameSort
User "GHC.Types.EQ" (Unique -> Int
getKey Unique
ordEQDataConKey) SrcSpan
wiredInSrcSpan
        GT -> NameSort -> OccName -> Int -> SrcSpan -> TyConName
forall a. NameSort -> OccName -> Int -> SrcSpan -> Name a
Name NameSort
User "GHC.Types.GT" (Unique -> Int
getKey Unique
ordGTDataConKey) SrcSpan
wiredInSrcSpan

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeSymbolCmpTyFamNameKey -- "GHC.TypeNats.CmpSymbol"
  , [s1 :: [Char]
s1, s2 :: [Char]
s2] <- (Type -> Maybe [Char]) -> [Type] -> [[Char]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe [Char]
symLitView TyConMap
tcm) [Type]
tys
  = 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
        LT -> NameSort -> OccName -> Int -> SrcSpan -> TyConName
forall a. NameSort -> OccName -> Int -> SrcSpan -> Name a
Name NameSort
User "GHC.Types.LT" (Unique -> Int
getKey Unique
ordLTDataConKey) SrcSpan
wiredInSrcSpan
        EQ -> NameSort -> OccName -> Int -> SrcSpan -> TyConName
forall a. NameSort -> OccName -> Int -> SrcSpan -> Name a
Name NameSort
User "GHC.Types.EQ" (Unique -> Int
getKey Unique
ordEQDataConKey) SrcSpan
wiredInSrcSpan
        GT -> NameSort -> OccName -> Int -> SrcSpan -> TyConName
forall a. NameSort -> OccName -> Int -> SrcSpan -> Name a
Name NameSort
User "GHC.Types.GT" (Unique -> Int
getKey Unique
ordGTDataConKey) SrcSpan
wiredInSrcSpan

  | TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
tc Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
typeSymbolAppendFamNameKey  -- GHC.TypeLits.AppendSymbol"
  , [s1 :: [Char]
s1, s2 :: [Char]
s2] <- (Type -> Maybe [Char]) -> [Type] -> [[Char]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe [Char]
symLitView TyConMap
tcm) [Type]
tys
  = 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)))

  | 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` ["GHC.TypeLits.Extra.FLog", "GHC.TypeNats.FLog"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , Integer
i1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 1
  , Integer
i2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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))))

  | 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` ["GHC.TypeLits.Extra.CLog", "GHC.TypeNats.CLog"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , Just k :: Int
k <- Integer -> Integer -> Maybe Int
clogBase Integer
i1 Integer
i2
  = Type -> Maybe Type
forall a. a -> Maybe a
Just (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
k)))

  | 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` ["GHC.TypeLits.Extra.Log", "GHC.TypeNats.Log"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , Integer
i1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 1
  , Integer
i2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 0
  = if Integer
i2 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1
       then Type -> Maybe Type
forall a. a -> Maybe a
Just (LitTy -> Type
LitTy (Integer -> LitTy
NumTy 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
-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)))


  | 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` ["GHC.TypeLits.Extra.GCD", "GHC.TypeNats.GCD"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (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 (Integer -> LitTy
NumTy (Integer
i1 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`gcd` Integer
i2)))

  | 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` ["GHC.TypeLits.Extra.LCM", "GHC.TypeNats.LCM"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (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 (Integer -> LitTy
NumTy (Integer
i1 Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`lcm` Integer
i2)))

  | 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` ["GHC.TypeLits.Extra.Div", "GHC.TypeNats.Div"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , Integer
i2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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)))

  | 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` ["GHC.TypeLits.Extra.Mod", "GHC.TypeNats.Mod"]
  , [i1 :: Integer
i1, i2 :: Integer
i2] <- (Type -> Maybe Integer) -> [Type] -> [Integer]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (TyConMap -> Type -> Maybe Integer
litView TyConMap
tcm) [Type]
tys
  , Integer
i2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> 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)))

  | 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
  = TyConMap -> [([Type], Type)] -> [Type] -> Maybe Type
findFunSubst TyConMap
tcm [([Type], Type)]
tcSubst [Type]
tys

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

-- |
isTypeFamilyApplication ::  TyConMap -> Type -> Bool
isTypeFamilyApplication :: TyConMap -> Type -> Bool
isTypeFamilyApplication tcm :: TyConMap
tcm (Type -> TypeView
tyView -> TyConApp tcNm :: TyConName
tcNm _args :: [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 _tcm :: TyConMap
_tcm _type :: Type
_type = Bool
False

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

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

-- | The type @forall a . a@
undefinedTy ::Type
undefinedTy :: Type
undefinedTy =
  let aNm :: Name a
aNm = OccName -> Int -> Name a
forall a. OccName -> Int -> Name a
mkUnsafeSystemName "a" 0
      aTv :: Var a
aTv = (Name a -> Int -> Type -> Var a
forall a. Name a -> Int -> Type -> Var a
TyVar Name a
forall a. Name a
aNm 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 nm :: TyConName
nm)) = TyConName -> Int
forall a. Name a -> Int
nameUniq TyConName
nm Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
getKey Unique
integerTyConKey
isIntegerTy _ = 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 tcMap :: TyConMap
tcMap = Type -> Type
go
  where
  go :: Type -> Type
go ty :: Type
ty = case Type -> TypeView
tyView Type
ty of
    TyConApp tcNm :: TyConName
tcNm args :: [Type]
args
      | TyConName -> OccName
forall a. Name a -> OccName
nameOcc TyConName
tcNm OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== "Clash.Signal.Internal.Signal"
      , [_,elTy :: Type
elTy] <- [Type]
args
      -> Type -> Type
go Type
elTy
      -- 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
== "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
== "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
== "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
== "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
== "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 _ nt :: ([TyVar], Type)
nt)}
             -> case ([TyVar], Type) -> [Type] -> Maybe Type
newTyConInstRhs ([TyVar], Type)
nt [Type]
args of
                  Just ty' :: Type
ty' -> Type -> Type
go Type
ty'
                  Nothing  -> Type
ty
          _ ->
             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
               Just ty'' :: Type
ty'' -> Type
ty''
               Nothing  -> Type
ty'
    FunTy ty1 :: Type
ty1 ty2 :: Type
ty2 -> Type -> Type -> Type
mkFunTy (Type -> Type
go Type
ty1) (Type -> Type
go Type
ty2)
    OtherType (ForAllTy tyvar :: TyVar
tyvar ty' :: Type
ty')
      -> TyVar -> Type -> Type
ForAllTy TyVar
tyvar (Type -> Type
go Type
ty')
    _ -> Type
ty

isClassTy
  :: TyConMap
  -> Type
  -> Bool
isClassTy :: TyConMap -> Type -> Bool
isClassTy tcm :: TyConMap
tcm (Type -> TypeView
tyView -> TyConApp tcNm :: TyConName
tcNm _) =
  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
    _ -> Bool
False
isClassTy _ _ = Bool
False