{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ViewPatterns #-}

-- | Definitions of and related to the sslang IR's type system.
module IR.Types.Type where

import Common.Identifiers (
  DConId (..),
  HasFreeVars (..),
  Identifiable,
  TConId (..),
  TVarId (..),
  fromId,
  fromString,
  reserved,
 )
import Common.Pretty (
  Dumpy (..),
  Pretty (pretty),
  brackets,
  comma,
  hsep,
  parens,
  (<+>),
 )

import Data.Foldable (toList)
import Data.Generics (
  Data,
  Typeable,
 )
import qualified Data.Map as M
import Data.Set ((\\))
import qualified Data.Set as S


{- | Encoding of sslang types.

Structurally speaking, these are very simple. Types are either type variables or
type constructors applied to some other types.

Builtin types (and type constructors) include 'Arrow', 'Unit', 'Ref', 'List',
and various sizes of tuples; for convenience, those are defined elsewhere using
the GHC PatternSynonyms extension.
-}
data Type
  = -- | Type constructor, applied to zero or more types
    TCon TConId [Type]
  | -- | Type variable (may be implicitly quantified)
    TVar TVarId
  deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Type] -> ShowS
$cshowList :: [Type] -> ShowS
show :: Type -> String
$cshow :: Type -> String
showsPrec :: Int -> Type -> ShowS
$cshowsPrec :: Int -> Type -> ShowS
Show, Typeable, Typeable Type
DataType
Constr
Typeable Type
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Type -> c Type)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Type)
-> (Type -> Constr)
-> (Type -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Type))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type))
-> ((forall b. Data b => b -> b) -> Type -> Type)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r)
-> (forall u. (forall d. Data d => d -> u) -> Type -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Type -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Type -> m Type)
-> Data Type
Type -> DataType
Type -> Constr
(forall b. Data b => b -> b) -> Type -> Type
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
forall u. (forall d. Data d => d -> u) -> Type -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cTVar :: Constr
$cTCon :: Constr
$tType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapMp :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapM :: (forall d. Data d => d -> m d) -> Type -> m Type
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Type -> m Type
gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Type -> u
gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Type -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r
gmapT :: (forall b. Data b => b -> b) -> Type -> Type
$cgmapT :: (forall b. Data b => b -> b) -> Type -> Type
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Type)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Type)
dataTypeOf :: Type -> DataType
$cdataTypeOf :: Type -> DataType
toConstr :: Type -> Constr
$ctoConstr :: Type -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Type
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Type -> c Type
$cp1Data :: Typeable Type
Data)


instance HasFreeVars Type TVarId where
  freeVars :: Type -> Set TVarId
freeVars (TCon TConId
_ [Type]
ts) = [Set TVarId] -> Set TVarId
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set TVarId] -> Set TVarId) -> [Set TVarId] -> Set TVarId
forall a b. (a -> b) -> a -> b
$ (Type -> Set TVarId) -> [Type] -> [Set TVarId]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Set TVarId
forall t i. HasFreeVars t i => t -> Set i
freeVars [Type]
ts
  freeVars Type
Hole = Set TVarId
forall a. Set a
S.empty
  freeVars (TVar TVarId
v) = TVarId -> Set TVarId
forall a. a -> Set a
S.singleton TVarId
v


{- | Constraints on a type scheme.

For now, we only support trivial constraints.
-}
data Constraint
  = -- | The trivial constraint, i.e., always satisfied.
    CTrue
  deriving (Constraint -> Constraint -> Bool
(Constraint -> Constraint -> Bool)
-> (Constraint -> Constraint -> Bool) -> Eq Constraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Constraint -> Constraint -> Bool
$c/= :: Constraint -> Constraint -> Bool
== :: Constraint -> Constraint -> Bool
$c== :: Constraint -> Constraint -> Bool
Eq, Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show, Typeable, Typeable Constraint
DataType
Constr
Typeable Constraint
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Constraint -> c Constraint)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Constraint)
-> (Constraint -> Constr)
-> (Constraint -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Constraint))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Constraint))
-> ((forall b. Data b => b -> b) -> Constraint -> Constraint)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Constraint -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Constraint -> r)
-> (forall u. (forall d. Data d => d -> u) -> Constraint -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Constraint -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Constraint -> m Constraint)
-> Data Constraint
Constraint -> DataType
Constraint -> Constr
(forall b. Data b => b -> b) -> Constraint -> Constraint
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Constraint -> u
forall u. (forall d. Data d => d -> u) -> Constraint -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constraint)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
$cCTrue :: Constr
$tConstraint :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapMp :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapM :: (forall d. Data d => d -> m d) -> Constraint -> m Constraint
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Constraint -> m Constraint
gmapQi :: Int -> (forall d. Data d => d -> u) -> Constraint -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Constraint -> u
gmapQ :: (forall d. Data d => d -> u) -> Constraint -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Constraint -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Constraint -> r
gmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint
$cgmapT :: (forall b. Data b => b -> b) -> Constraint -> Constraint
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Constraint)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Constraint)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Constraint)
dataTypeOf :: Constraint -> DataType
$cdataTypeOf :: Constraint -> DataType
toConstr :: Constraint -> Constr
$ctoConstr :: Constraint -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Constraint
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Constraint -> c Constraint
$cp1Data :: Typeable Constraint
Data)


{- | Schemes quantify over 'Type' variables and impose some 'Constraint'.

'SchemeOf' is implemented as functor over some kind of type so we can easily
substitute in 'Type' vs 'UType' when performing type inference/unification.
-}
data SchemeOf t = Forall (S.Set TVarId) Constraint t
  deriving (SchemeOf t -> SchemeOf t -> Bool
(SchemeOf t -> SchemeOf t -> Bool)
-> (SchemeOf t -> SchemeOf t -> Bool) -> Eq (SchemeOf t)
forall t. Eq t => SchemeOf t -> SchemeOf t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SchemeOf t -> SchemeOf t -> Bool
$c/= :: forall t. Eq t => SchemeOf t -> SchemeOf t -> Bool
== :: SchemeOf t -> SchemeOf t -> Bool
$c== :: forall t. Eq t => SchemeOf t -> SchemeOf t -> Bool
Eq, Int -> SchemeOf t -> ShowS
[SchemeOf t] -> ShowS
SchemeOf t -> String
(Int -> SchemeOf t -> ShowS)
-> (SchemeOf t -> String)
-> ([SchemeOf t] -> ShowS)
-> Show (SchemeOf t)
forall t. Show t => Int -> SchemeOf t -> ShowS
forall t. Show t => [SchemeOf t] -> ShowS
forall t. Show t => SchemeOf t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SchemeOf t] -> ShowS
$cshowList :: forall t. Show t => [SchemeOf t] -> ShowS
show :: SchemeOf t -> String
$cshow :: forall t. Show t => SchemeOf t -> String
showsPrec :: Int -> SchemeOf t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> SchemeOf t -> ShowS
Show, a -> SchemeOf b -> SchemeOf a
(a -> b) -> SchemeOf a -> SchemeOf b
(forall a b. (a -> b) -> SchemeOf a -> SchemeOf b)
-> (forall a b. a -> SchemeOf b -> SchemeOf a) -> Functor SchemeOf
forall a b. a -> SchemeOf b -> SchemeOf a
forall a b. (a -> b) -> SchemeOf a -> SchemeOf b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SchemeOf b -> SchemeOf a
$c<$ :: forall a b. a -> SchemeOf b -> SchemeOf a
fmap :: (a -> b) -> SchemeOf a -> SchemeOf b
$cfmap :: forall a b. (a -> b) -> SchemeOf a -> SchemeOf b
Functor, SchemeOf a -> Bool
(a -> m) -> SchemeOf a -> m
(a -> b -> b) -> b -> SchemeOf a -> b
(forall m. Monoid m => SchemeOf m -> m)
-> (forall m a. Monoid m => (a -> m) -> SchemeOf a -> m)
-> (forall m a. Monoid m => (a -> m) -> SchemeOf a -> m)
-> (forall a b. (a -> b -> b) -> b -> SchemeOf a -> b)
-> (forall a b. (a -> b -> b) -> b -> SchemeOf a -> b)
-> (forall b a. (b -> a -> b) -> b -> SchemeOf a -> b)
-> (forall b a. (b -> a -> b) -> b -> SchemeOf a -> b)
-> (forall a. (a -> a -> a) -> SchemeOf a -> a)
-> (forall a. (a -> a -> a) -> SchemeOf a -> a)
-> (forall a. SchemeOf a -> [a])
-> (forall a. SchemeOf a -> Bool)
-> (forall a. SchemeOf a -> Int)
-> (forall a. Eq a => a -> SchemeOf a -> Bool)
-> (forall a. Ord a => SchemeOf a -> a)
-> (forall a. Ord a => SchemeOf a -> a)
-> (forall a. Num a => SchemeOf a -> a)
-> (forall a. Num a => SchemeOf a -> a)
-> Foldable SchemeOf
forall a. Eq a => a -> SchemeOf a -> Bool
forall a. Num a => SchemeOf a -> a
forall a. Ord a => SchemeOf a -> a
forall m. Monoid m => SchemeOf m -> m
forall a. SchemeOf a -> Bool
forall a. SchemeOf a -> Int
forall a. SchemeOf a -> [a]
forall a. (a -> a -> a) -> SchemeOf a -> a
forall m a. Monoid m => (a -> m) -> SchemeOf a -> m
forall b a. (b -> a -> b) -> b -> SchemeOf a -> b
forall a b. (a -> b -> b) -> b -> SchemeOf a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: SchemeOf a -> a
$cproduct :: forall a. Num a => SchemeOf a -> a
sum :: SchemeOf a -> a
$csum :: forall a. Num a => SchemeOf a -> a
minimum :: SchemeOf a -> a
$cminimum :: forall a. Ord a => SchemeOf a -> a
maximum :: SchemeOf a -> a
$cmaximum :: forall a. Ord a => SchemeOf a -> a
elem :: a -> SchemeOf a -> Bool
$celem :: forall a. Eq a => a -> SchemeOf a -> Bool
length :: SchemeOf a -> Int
$clength :: forall a. SchemeOf a -> Int
null :: SchemeOf a -> Bool
$cnull :: forall a. SchemeOf a -> Bool
toList :: SchemeOf a -> [a]
$ctoList :: forall a. SchemeOf a -> [a]
foldl1 :: (a -> a -> a) -> SchemeOf a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SchemeOf a -> a
foldr1 :: (a -> a -> a) -> SchemeOf a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SchemeOf a -> a
foldl' :: (b -> a -> b) -> b -> SchemeOf a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SchemeOf a -> b
foldl :: (b -> a -> b) -> b -> SchemeOf a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SchemeOf a -> b
foldr' :: (a -> b -> b) -> b -> SchemeOf a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SchemeOf a -> b
foldr :: (a -> b -> b) -> b -> SchemeOf a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SchemeOf a -> b
foldMap' :: (a -> m) -> SchemeOf a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SchemeOf a -> m
foldMap :: (a -> m) -> SchemeOf a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SchemeOf a -> m
fold :: SchemeOf m -> m
$cfold :: forall m. Monoid m => SchemeOf m -> m
Foldable, Functor SchemeOf
Foldable SchemeOf
Functor SchemeOf
-> Foldable SchemeOf
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SchemeOf a -> f (SchemeOf b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SchemeOf (f a) -> f (SchemeOf a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SchemeOf a -> m (SchemeOf b))
-> (forall (m :: * -> *) a.
    Monad m =>
    SchemeOf (m a) -> m (SchemeOf a))
-> Traversable SchemeOf
(a -> f b) -> SchemeOf a -> f (SchemeOf b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => SchemeOf (m a) -> m (SchemeOf a)
forall (f :: * -> *) a.
Applicative f =>
SchemeOf (f a) -> f (SchemeOf a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SchemeOf a -> m (SchemeOf b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SchemeOf a -> f (SchemeOf b)
sequence :: SchemeOf (m a) -> m (SchemeOf a)
$csequence :: forall (m :: * -> *) a. Monad m => SchemeOf (m a) -> m (SchemeOf a)
mapM :: (a -> m b) -> SchemeOf a -> m (SchemeOf b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SchemeOf a -> m (SchemeOf b)
sequenceA :: SchemeOf (f a) -> f (SchemeOf a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SchemeOf (f a) -> f (SchemeOf a)
traverse :: (a -> f b) -> SchemeOf a -> f (SchemeOf b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SchemeOf a -> f (SchemeOf b)
$cp2Traversable :: Foldable SchemeOf
$cp1Traversable :: Functor SchemeOf
Traversable, Typeable, Typeable (SchemeOf t)
DataType
Constr
Typeable (SchemeOf t)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SchemeOf t -> c (SchemeOf t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (SchemeOf t))
-> (SchemeOf t -> Constr)
-> (SchemeOf t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (SchemeOf t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (SchemeOf t)))
-> ((forall b. Data b => b -> b) -> SchemeOf t -> SchemeOf t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r)
-> (forall u. (forall d. Data d => d -> u) -> SchemeOf t -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SchemeOf t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t))
-> Data (SchemeOf t)
SchemeOf t -> DataType
SchemeOf t -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (SchemeOf t))
(forall b. Data b => b -> b) -> SchemeOf t -> SchemeOf t
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SchemeOf t -> c (SchemeOf t)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SchemeOf t)
forall t. Data t => Typeable (SchemeOf t)
forall t. Data t => SchemeOf t -> DataType
forall t. Data t => SchemeOf t -> Constr
forall t.
Data t =>
(forall b. Data b => b -> b) -> SchemeOf t -> SchemeOf t
forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> SchemeOf t -> u
forall t u.
Data t =>
(forall d. Data d => d -> u) -> SchemeOf t -> [u]
forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SchemeOf t)
forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SchemeOf t -> c (SchemeOf t)
forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SchemeOf t))
forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SchemeOf t))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SchemeOf t -> u
forall u. (forall d. Data d => d -> u) -> SchemeOf t -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SchemeOf t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SchemeOf t -> c (SchemeOf t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (SchemeOf t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SchemeOf t))
$cForall :: Constr
$tSchemeOf :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
$cgmapMo :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
gmapMp :: (forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
$cgmapMp :: forall t (m :: * -> *).
(Data t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
gmapM :: (forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
$cgmapM :: forall t (m :: * -> *).
(Data t, Monad m) =>
(forall d. Data d => d -> m d) -> SchemeOf t -> m (SchemeOf t)
gmapQi :: Int -> (forall d. Data d => d -> u) -> SchemeOf t -> u
$cgmapQi :: forall t u.
Data t =>
Int -> (forall d. Data d => d -> u) -> SchemeOf t -> u
gmapQ :: (forall d. Data d => d -> u) -> SchemeOf t -> [u]
$cgmapQ :: forall t u.
Data t =>
(forall d. Data d => d -> u) -> SchemeOf t -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
$cgmapQr :: forall t r r'.
Data t =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
$cgmapQl :: forall t r r'.
Data t =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SchemeOf t -> r
gmapT :: (forall b. Data b => b -> b) -> SchemeOf t -> SchemeOf t
$cgmapT :: forall t.
Data t =>
(forall b. Data b => b -> b) -> SchemeOf t -> SchemeOf t
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SchemeOf t))
$cdataCast2 :: forall t (t :: * -> * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (SchemeOf t))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (SchemeOf t))
$cdataCast1 :: forall t (t :: * -> *) (c :: * -> *).
(Data t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (SchemeOf t))
dataTypeOf :: SchemeOf t -> DataType
$cdataTypeOf :: forall t. Data t => SchemeOf t -> DataType
toConstr :: SchemeOf t -> Constr
$ctoConstr :: forall t. Data t => SchemeOf t -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SchemeOf t)
$cgunfold :: forall t (c :: * -> *).
Data t =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (SchemeOf t)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SchemeOf t -> c (SchemeOf t)
$cgfoldl :: forall t (c :: * -> *).
Data t =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SchemeOf t -> c (SchemeOf t)
$cp1Data :: forall t. Data t => Typeable (SchemeOf t)
Data)


-- | Unwrap a scheme and obtain the underlying type.
unScheme :: SchemeOf t -> t
unScheme :: SchemeOf t -> t
unScheme (Forall Set TVarId
_ Constraint
_ t
t) = t
t


-- | Construct a scheme with quantified type variables and a trivial constraint.
forall :: (Functor l, Foldable l) => l TVarId -> t -> SchemeOf t
forall :: l TVarId -> t -> SchemeOf t
forall l TVarId
vs = Set TVarId -> Constraint -> t -> SchemeOf t
forall t. Set TVarId -> Constraint -> t -> SchemeOf t
Forall ([TVarId] -> Set TVarId
forall a. Ord a => [a] -> Set a
S.fromList ([TVarId] -> Set TVarId) -> [TVarId] -> Set TVarId
forall a b. (a -> b) -> a -> b
$ l TVarId -> [TVarId]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (l TVarId -> [TVarId]) -> l TVarId -> [TVarId]
forall a b. (a -> b) -> a -> b
$ (TVarId -> TVarId) -> l TVarId -> l TVarId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TVarId -> TVarId
forall a b. (Identifiable a, Identifiable b) => a -> b
fromId l TVarId
vs) Constraint
CTrue


-- | Construct a scheme from all free type variables and a trivial constraint.
schemeOf :: Type -> Scheme
schemeOf :: Type -> Scheme
schemeOf Type
t = SchemeOf Type -> Scheme
Scheme (SchemeOf Type -> Scheme) -> SchemeOf Type -> Scheme
forall a b. (a -> b) -> a -> b
$ [TVarId] -> Type -> SchemeOf Type
forall (l :: * -> *) t.
(Functor l, Foldable l) =>
l TVarId -> t -> SchemeOf t
forall (Set TVarId -> [TVarId]
forall a. Set a -> [a]
S.toList (Set TVarId -> [TVarId]) -> Set TVarId -> [TVarId]
forall a b. (a -> b) -> a -> b
$ Type -> Set TVarId
forall t i. HasFreeVars t i => t -> Set i
freeVars Type
t) Type
t


-- | Schemes over 'Type'.
newtype Scheme = Scheme (SchemeOf Type)
  deriving (Scheme -> Scheme -> Bool
(Scheme -> Scheme -> Bool)
-> (Scheme -> Scheme -> Bool) -> Eq Scheme
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Scheme -> Scheme -> Bool
$c/= :: Scheme -> Scheme -> Bool
== :: Scheme -> Scheme -> Bool
$c== :: Scheme -> Scheme -> Bool
Eq, Int -> Scheme -> ShowS
[Scheme] -> ShowS
Scheme -> String
(Int -> Scheme -> ShowS)
-> (Scheme -> String) -> ([Scheme] -> ShowS) -> Show Scheme
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Scheme] -> ShowS
$cshowList :: [Scheme] -> ShowS
show :: Scheme -> String
$cshow :: Scheme -> String
showsPrec :: Int -> Scheme -> ShowS
$cshowsPrec :: Int -> Scheme -> ShowS
Show, Typeable, Typeable Scheme
DataType
Constr
Typeable Scheme
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Scheme -> c Scheme)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Scheme)
-> (Scheme -> Constr)
-> (Scheme -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Scheme))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scheme))
-> ((forall b. Data b => b -> b) -> Scheme -> Scheme)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Scheme -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Scheme -> r)
-> (forall u. (forall d. Data d => d -> u) -> Scheme -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Scheme -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Scheme -> m Scheme)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Scheme -> m Scheme)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Scheme -> m Scheme)
-> Data Scheme
Scheme -> DataType
Scheme -> Constr
(forall b. Data b => b -> b) -> Scheme -> Scheme
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scheme -> c Scheme
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scheme
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Scheme -> u
forall u. (forall d. Data d => d -> u) -> Scheme -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scheme -> m Scheme
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scheme -> m Scheme
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scheme
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scheme -> c Scheme
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scheme)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scheme)
$cScheme :: Constr
$tScheme :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Scheme -> m Scheme
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scheme -> m Scheme
gmapMp :: (forall d. Data d => d -> m d) -> Scheme -> m Scheme
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Scheme -> m Scheme
gmapM :: (forall d. Data d => d -> m d) -> Scheme -> m Scheme
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Scheme -> m Scheme
gmapQi :: Int -> (forall d. Data d => d -> u) -> Scheme -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Scheme -> u
gmapQ :: (forall d. Data d => d -> u) -> Scheme -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Scheme -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scheme -> r
gmapT :: (forall b. Data b => b -> b) -> Scheme -> Scheme
$cgmapT :: (forall b. Data b => b -> b) -> Scheme -> Scheme
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scheme)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Scheme)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Scheme)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Scheme)
dataTypeOf :: Scheme -> DataType
$cdataTypeOf :: Scheme -> DataType
toConstr :: Scheme -> Constr
$ctoConstr :: Scheme -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scheme
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Scheme
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scheme -> c Scheme
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Scheme -> c Scheme
$cp1Data :: Typeable Scheme
Data)


instance HasFreeVars Scheme TVarId where
  freeVars :: Scheme -> Set TVarId
freeVars (Scheme (Forall Set TVarId
s Constraint
_ Type
t)) = Type -> Set TVarId
forall t i. HasFreeVars t i => t -> Set i
freeVars Type
t Set TVarId -> Set TVarId -> Set TVarId
forall a. Ord a => Set a -> Set a -> Set a
\\ Set TVarId
s


-- | An annotation records the annotated portion of a pattern.
data Annotation
  = -- | A basic 'Type' annotation
    AnnType Type
  | -- | Annotations collected from patterns
    AnnDCon DConId [Annotation]
  | -- | Annotations collected from fun args
    AnnArrows [Annotation] Annotation
  deriving (Annotation -> Annotation -> Bool
(Annotation -> Annotation -> Bool)
-> (Annotation -> Annotation -> Bool) -> Eq Annotation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Annotation -> Annotation -> Bool
$c/= :: Annotation -> Annotation -> Bool
== :: Annotation -> Annotation -> Bool
$c== :: Annotation -> Annotation -> Bool
Eq, Int -> Annotation -> ShowS
[Annotation] -> ShowS
Annotation -> String
(Int -> Annotation -> ShowS)
-> (Annotation -> String)
-> ([Annotation] -> ShowS)
-> Show Annotation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Annotation] -> ShowS
$cshowList :: [Annotation] -> ShowS
show :: Annotation -> String
$cshow :: Annotation -> String
showsPrec :: Int -> Annotation -> ShowS
$cshowsPrec :: Int -> Annotation -> ShowS
Show, Typeable, Typeable Annotation
DataType
Constr
Typeable Annotation
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Annotation -> c Annotation)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Annotation)
-> (Annotation -> Constr)
-> (Annotation -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Annotation))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Annotation))
-> ((forall b. Data b => b -> b) -> Annotation -> Annotation)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Annotation -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Annotation -> r)
-> (forall u. (forall d. Data d => d -> u) -> Annotation -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Annotation -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Annotation -> m Annotation)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Annotation -> m Annotation)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Annotation -> m Annotation)
-> Data Annotation
Annotation -> DataType
Annotation -> Constr
(forall b. Data b => b -> b) -> Annotation -> Annotation
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotation -> c Annotation
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotation
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Annotation -> u
forall u. (forall d. Data d => d -> u) -> Annotation -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotation -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotation -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotation -> m Annotation
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotation -> m Annotation
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotation
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotation -> c Annotation
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotation)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotation)
$cAnnArrows :: Constr
$cAnnDCon :: Constr
$cAnnType :: Constr
$tAnnotation :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Annotation -> m Annotation
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotation -> m Annotation
gmapMp :: (forall d. Data d => d -> m d) -> Annotation -> m Annotation
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotation -> m Annotation
gmapM :: (forall d. Data d => d -> m d) -> Annotation -> m Annotation
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotation -> m Annotation
gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotation -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Annotation -> u
gmapQ :: (forall d. Data d => d -> u) -> Annotation -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Annotation -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotation -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotation -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotation -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotation -> r
gmapT :: (forall b. Data b => b -> b) -> Annotation -> Annotation
$cgmapT :: (forall b. Data b => b -> b) -> Annotation -> Annotation
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotation)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Annotation)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Annotation)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotation)
dataTypeOf :: Annotation -> DataType
$cdataTypeOf :: Annotation -> DataType
toConstr :: Annotation -> Constr
$ctoConstr :: Annotation -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotation
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotation
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotation -> c Annotation
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotation -> c Annotation
$cp1Data :: Typeable Annotation
Data)


-- | Expressions are annotated with a (potentially empty) list of 'Annotation'.
newtype Annotations = Annotations [Annotation]
  deriving (Annotations -> Annotations -> Bool
(Annotations -> Annotations -> Bool)
-> (Annotations -> Annotations -> Bool) -> Eq Annotations
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Annotations -> Annotations -> Bool
$c/= :: Annotations -> Annotations -> Bool
== :: Annotations -> Annotations -> Bool
$c== :: Annotations -> Annotations -> Bool
Eq, Int -> Annotations -> ShowS
[Annotations] -> ShowS
Annotations -> String
(Int -> Annotations -> ShowS)
-> (Annotations -> String)
-> ([Annotations] -> ShowS)
-> Show Annotations
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Annotations] -> ShowS
$cshowList :: [Annotations] -> ShowS
show :: Annotations -> String
$cshow :: Annotations -> String
showsPrec :: Int -> Annotations -> ShowS
$cshowsPrec :: Int -> Annotations -> ShowS
Show, Typeable, Typeable Annotations
DataType
Constr
Typeable Annotations
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Annotations -> c Annotations)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Annotations)
-> (Annotations -> Constr)
-> (Annotations -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Annotations))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c Annotations))
-> ((forall b. Data b => b -> b) -> Annotations -> Annotations)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Annotations -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Annotations -> r)
-> (forall u. (forall d. Data d => d -> u) -> Annotations -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Annotations -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Annotations -> m Annotations)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Annotations -> m Annotations)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Annotations -> m Annotations)
-> Data Annotations
Annotations -> DataType
Annotations -> Constr
(forall b. Data b => b -> b) -> Annotations -> Annotations
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Annotations -> u
forall u. (forall d. Data d => d -> u) -> Annotations -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotations)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Annotations)
$cAnnotations :: Constr
$tAnnotations :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Annotations -> m Annotations
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
gmapMp :: (forall d. Data d => d -> m d) -> Annotations -> m Annotations
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
gmapM :: (forall d. Data d => d -> m d) -> Annotations -> m Annotations
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Annotations -> m Annotations
gmapQi :: Int -> (forall d. Data d => d -> u) -> Annotations -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Annotations -> u
gmapQ :: (forall d. Data d => d -> u) -> Annotations -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Annotations -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Annotations -> r
gmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations
$cgmapT :: (forall b. Data b => b -> b) -> Annotations -> Annotations
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Annotations)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c Annotations)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Annotations)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Annotations)
dataTypeOf :: Annotations -> DataType
$cdataTypeOf :: Annotations -> DataType
toConstr :: Annotations -> Constr
$ctoConstr :: Annotations -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Annotations
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Annotations -> c Annotations
$cp1Data :: Typeable Annotations
Data, b -> Annotations -> Annotations
NonEmpty Annotations -> Annotations
Annotations -> Annotations -> Annotations
(Annotations -> Annotations -> Annotations)
-> (NonEmpty Annotations -> Annotations)
-> (forall b. Integral b => b -> Annotations -> Annotations)
-> Semigroup Annotations
forall b. Integral b => b -> Annotations -> Annotations
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> Annotations -> Annotations
$cstimes :: forall b. Integral b => b -> Annotations -> Annotations
sconcat :: NonEmpty Annotations -> Annotations
$csconcat :: NonEmpty Annotations -> Annotations
<> :: Annotations -> Annotations -> Annotations
$c<> :: Annotations -> Annotations -> Annotations
Semigroup, Semigroup Annotations
Annotations
Semigroup Annotations
-> Annotations
-> (Annotations -> Annotations -> Annotations)
-> ([Annotations] -> Annotations)
-> Monoid Annotations
[Annotations] -> Annotations
Annotations -> Annotations -> Annotations
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Annotations] -> Annotations
$cmconcat :: [Annotations] -> Annotations
mappend :: Annotations -> Annotations -> Annotations
$cmappend :: Annotations -> Annotations -> Annotations
mempty :: Annotations
$cmempty :: Annotations
$cp1Monoid :: Semigroup Annotations
Monoid)


-- | Unwrap the 'Annotations' data constructor.
unAnnotations :: Annotations -> [Annotation]
unAnnotations :: Annotations -> [Annotation]
unAnnotations (Annotations [Annotation]
as) = [Annotation]
as


{- | Unroll an annotation into a type.
 FIXME: get rid of this.
-}
fromAnnotations :: Annotations -> Type
fromAnnotations :: Annotations -> Type
fromAnnotations = [Annotation] -> Type
go ([Annotation] -> Type)
-> (Annotations -> [Annotation]) -> Annotations -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annotations -> [Annotation]
unAnnotations
 where
  go :: [Annotation] -> Type
go (AnnType Type
t : [Annotation]
_) = Type
t
  go (Annotation
_ : [Annotation]
anns) = [Annotation] -> Type
go [Annotation]
anns
  go [] = Type
Hole -- TODO: properly unroll


-- | Some data type that contains a sslang 'Type'.
class HasType a where
  getType :: a -> Type


instance HasType Type where
  getType :: Type -> Type
getType = Type -> Type
forall a. a -> a
id


instance HasType Scheme where
  getType :: Scheme -> Type
getType (Scheme (Forall Set TVarId
_ Constraint
_ Type
t)) = Type
t


-- | A fresh, free type variable; may appear in type annotations.
pattern Hole :: Type
pattern $bHole :: Type
$mHole :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
Hole = TVar "_"


-- | The type constructor for function arrows.
pattern Arrow :: Type -> Type -> Type
pattern $bArrow :: Type -> Type -> Type
$mArrow :: forall r. Type -> (Type -> Type -> r) -> (Void# -> r) -> r
Arrow a b = TCon "->" [a, b]


-- | Unfold an 'Arrow' 'Type' into a list of argument types and a return type.
unfoldArrow :: Type -> ([Type], Type)
unfoldArrow :: Type -> ([Type], Type)
unfoldArrow (Arrow Type
a Type
b) = let ([Type]
as, Type
rt) = Type -> ([Type], Type)
unfoldArrow Type
b in (Type
a Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
as, Type
rt)
unfoldArrow Type
t = ([], Type
t)


-- | Fold a list of argument types and a return type into an 'Arrow' 'Type'.
foldArrow :: ([Type], Type) -> Type
foldArrow :: ([Type], Type) -> Type
foldArrow (Type
a : [Type]
as, Type
rt) = Type
a Type -> Type -> Type
`Arrow` ([Type], Type) -> Type
foldArrow ([Type]
as, Type
rt)
foldArrow ([], Type
t) = Type
t


-- | The builtin singleton 'Type', whose only data constructor is just @()@.
pattern Unit :: Type
pattern $bUnit :: Type
$mUnit :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
Unit = TCon "()" []


-- | The builtin reference 'Type', created using @new@.
pattern Ref :: Type -> Type
pattern $bRef :: Type -> Type
$mRef :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
Ref a = TCon "&" [a]


-- | The builtin list 'Type', created using list syntax, e.g., @[a, b]@.
pattern List :: Type -> Type
pattern $bList :: Type -> Type
$mList :: forall r. Type -> (Type -> r) -> (Void# -> r) -> r
List a = TCon "[]" [a]


-- | The builtin 64-bit timestamp 'Type'.
pattern Time :: Type
pattern $bTime :: Type
$mTime :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
Time = TCon "Time" []


-- | Builtin 'Type' for signed 64-bit integers.
pattern I64 :: Type
pattern $bI64 :: Type
$mI64 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I64 = TCon "Int64" []


-- | Builtin 'Type' for unsigned 64-bit integers.
pattern U64 :: Type
pattern $bU64 :: Type
$mU64 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U64 = TCon "UInt64" []


-- | Builtin 'Type' for signed 32-bit integers.
pattern I32 :: Type
pattern $bI32 :: Type
$mI32 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I32 = TCon "Int32" []


-- | Builtin 'Type' for unsigned 32-bit integers.
pattern U32 :: Type
pattern $bU32 :: Type
$mU32 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U32 = TCon "UInt32" []


-- | Builtin 'Type' for signed 16-bit integers.
pattern I16 :: Type
pattern $bI16 :: Type
$mI16 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I16 = TCon "Int16" []


-- | Builtin 'Type' for unsigned 16-bit integers.
pattern U16 :: Type
pattern $bU16 :: Type
$mU16 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U16 = TCon "UInt16" []


-- | Builtin 'Type' for signed 8-bit integers.
pattern I8 :: Type
pattern $bI8 :: Type
$mI8 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
I8 = TCon "Int8" []


-- | Builtin 'Type' for unsigned 8-bit integers.
pattern U8 :: Type
pattern $bU8 :: Type
$mU8 :: forall r. Type -> (Void# -> r) -> (Void# -> r) -> r
U8 = TCon "UInt8" []


-- | Test whether a 'Type' is one of the builtin signed integers.
isInt :: Type -> Bool
isInt :: Type -> Bool
isInt Type
I64 = Bool
True
isInt Type
I32 = Bool
True
isInt Type
I16 = Bool
True
isInt Type
I8 = Bool
True
isInt Type
_ = Bool
False


-- | Test whether a 'Type' is one of the builtin unsigned integers.
isUInt :: Type -> Bool
isUInt :: Type -> Bool
isUInt Type
U64 = Bool
True
isUInt Type
U32 = Bool
True
isUInt Type
U16 = Bool
True
isUInt Type
U8 = Bool
True
isUInt Type
_ = Bool
False


-- | Test whether a 'Type' is one of the builtin numeric types.
isNum :: Type -> Bool
isNum :: Type -> Bool
isNum Type
t = Type -> Bool
isInt Type
t Bool -> Bool -> Bool
|| Type -> Bool
isUInt Type
t


-- | Construct a builtin tuple type out of a list of at least 2 types.
tuple :: [Type] -> Type
tuple :: [Type] -> Type
tuple [Type]
ts
  | [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 = TConId -> [Type] -> Type
TCon (Int -> TConId
forall v. Identifiable v => Int -> v
tupleId (Int -> TConId) -> Int -> TConId
forall a b. (a -> b) -> a -> b
$ [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts) [Type]
ts
  | Bool
otherwise = String -> Type
forall a. HasCallStack => String -> a
error (String -> Type) -> String -> Type
forall a b. (a -> b) -> a -> b
$ String
"Cannot create tuple of arity: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)


-- | Construct the type constructor of a builtin tuple of given arity (>= 2).
tupleId :: Identifiable v => Int -> v
tupleId :: Int -> v
tupleId Int
i
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 = v -> v
forall a. Identifiable a => a -> a
reserved (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ String -> v
forall a. IsString a => String -> a
fromString (String
"tuple" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)
  | Bool
otherwise = String -> v
forall a. HasCallStack => String -> a
error (String -> v) -> String -> v
forall a b. (a -> b) -> a -> b
$ String
"Cannot create tuple of arity: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i


-- | Kinds are just the arity of type constructors.
type Kind = Int


-- | Map to help us look up the kinds of builtin types.
builtinKinds :: M.Map TConId Kind
builtinKinds :: Map TConId Int
builtinKinds =
  [(TConId, Int)] -> Map TConId Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(TConId, Int)] -> Map TConId Int)
-> [(TConId, Int)] -> Map TConId Int
forall a b. (a -> b) -> a -> b
$
    [ Type -> (TConId, Int)
k (Type -> (TConId, Int)) -> Type -> (TConId, Int)
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
TVar TVarId
"a" Type -> Type -> Type
`Arrow` TVarId -> Type
TVar TVarId
"b"
    , Type -> (TConId, Int)
k Type
Unit
    , Type -> (TConId, Int)
k (Type -> (TConId, Int)) -> Type -> (TConId, Int)
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ref (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
TVar TVarId
"a"
    , Type -> (TConId, Int)
k (Type -> (TConId, Int)) -> Type -> (TConId, Int)
forall a b. (a -> b) -> a -> b
$ Type -> Type
List (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TVarId -> Type
TVar TVarId
"a"
    , Type -> (TConId, Int)
k Type
Time
    , Type -> (TConId, Int)
k Type
I64
    , Type -> (TConId, Int)
k Type
U64
    , Type -> (TConId, Int)
k Type
I32
    , Type -> (TConId, Int)
k Type
U32
    , Type -> (TConId, Int)
k Type
I16
    , Type -> (TConId, Int)
k Type
U16
    , Type -> (TConId, Int)
k Type
I8
    , Type -> (TConId, Int)
k Type
U8
    , (TConId
"(,)", Int
2)
    , (TConId
"(,,)", Int
3)
    ]
      [(TConId, Int)] -> [(TConId, Int)] -> [(TConId, Int)]
forall a. [a] -> [a] -> [a]
++ Int -> [(TConId, Int)] -> [(TConId, Int)]
forall a. Int -> [a] -> [a]
take Int
8 ((Int -> (TConId, Int)) -> [Int] -> [(TConId, Int)]
forall a b. (a -> b) -> [a] -> [b]
map Int -> (TConId, Int)
forall a b. (Identifiable a, Num b) => Int -> (a, b)
tup [(Int
2 :: Int) ..])
 where
  k :: Type -> (TConId, Int)
k (TCon TConId
tc [Type]
ts) = (TConId
tc, [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)
  k Type
_ = String -> (TConId, Int)
forall a. HasCallStack => String -> a
error String
"This should only be used with (builtin) TCons"
  tup :: Int -> (a, b)
tup Int
i = (Int -> a
forall v. Identifiable v => Int -> v
tupleId Int
i, b
2)


instance Pretty Type where
  pretty :: Type -> Doc ann
pretty (Arrow Type
a Type
b) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Type
a Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Type
b
  pretty (List Type
a) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Type
a
  pretty (TCon TConId
n []) = TConId -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty TConId
n
  pretty (TCon TConId
n [Type]
ts) = Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep (TConId -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty TConId
n Doc ann -> [Doc ann] -> [Doc ann]
forall a. a -> [a] -> [a]
: (Type -> Doc ann) -> [Type] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty [Type]
ts)
  pretty (TVar TVarId
n) = TVarId -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty TVarId
n


instance Dumpy Type where
  dumpy :: Type -> Doc ann
dumpy = Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty


instance Pretty Scheme where
  pretty :: Scheme -> Doc ann
pretty (Scheme (Forall Set TVarId
tvs Constraint
CTrue Type
t)) =
    String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String
"forall" :: String)
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ((TVarId -> Doc ann) -> [TVarId] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map TVarId -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([TVarId] -> [Doc ann]) -> [TVarId] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Set TVarId -> [TVarId]
forall a. Set a -> [a]
S.toList Set TVarId
tvs)
        Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
comma
      Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Type
t


instance Dumpy Scheme where
  dumpy :: Scheme -> Doc ann
dumpy = Scheme -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty


instance Pretty Annotation where
  pretty :: Annotation -> Doc ann
pretty (AnnType Type
t) = Type -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Type
t
  pretty Annotation
_ = Doc ann
forall a. Monoid a => a
mempty


instance Dumpy Annotation where
  dumpy :: Annotation -> Doc ann
dumpy = Annotation -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty


instance Pretty Annotations where
  pretty :: Annotations -> Doc ann
pretty (Annotations -> [Annotation]
unAnnotations -> [Annotation]
as)
    | [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annotation]
as = Doc ann
forall a. Monoid a => a
mempty
    | Bool
otherwise = Annotation -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Annotation -> Doc ann) -> Annotation -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Annotation] -> Annotation
forall a. [a] -> a
head [Annotation]
as


instance Dumpy Annotations where
  dumpy :: Annotations -> Doc ann
dumpy = Annotations -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty