{-# LANGUAGE CPP                       #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE ViewPatterns              #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE StandaloneDeriving        #-}

-- | This module contains a wrappers and utility functions for
-- accessing GHC module information. It should NEVER depend on
module Language.Haskell.Liquid.GHC.TypeRep (
  mkTyArg, 

  showTy
  ) where

import Coercion
import CoAxiom

import           Language.Haskell.Liquid.GHC.Misc (showPpr)
import           Language.Haskell.Liquid.GHC.API as Ghc hiding (mkTyArg)
import           Language.Fixpoint.Types (symbol)

-- e368f3265b80aeb337fbac3f6a70ee54ab14edfd

mkTyArg :: TyVar -> TyVarBinder
mkTyArg :: TyVar -> TyVarBinder
mkTyArg TyVar
v = TyVar -> ArgFlag -> TyVarBinder
forall var argf. var -> argf -> VarBndr var argf
Bndr TyVar
v ArgFlag
Required

instance Eq Type where
  Type
t1 == :: Type -> Type -> Bool
== Type
t2 = Type -> Type -> Bool
eqType' Type
t1 Type
t2

eqType' :: Type -> Type -> Bool 
eqType' :: Type -> Type -> Bool
eqType' (LitTy TyLit
l1) (LitTy TyLit
l2) 
  = TyLit
l1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
l2  
eqType' (CoercionTy Coercion
c1) (CoercionTy Coercion
c2) 
  = Coercion
c1 Coercion -> Coercion -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion
c2  
eqType'(CastTy Type
t1 Coercion
c1) (CastTy Type
t2 Coercion
c2) 
  = Type -> Type -> Bool
eqType' Type
t1 Type
t2 Bool -> Bool -> Bool
&& Coercion
c1 Coercion -> Coercion -> Bool
forall a. Eq a => a -> a -> Bool
== Coercion
c2 
eqType' (FunTy AnonArgFlag
a1 Type
t11 Type
t12) (FunTy AnonArgFlag
a2 Type
t21 Type
t22)
  = AnonArgFlag
a1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
a2 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t11 Type
t21 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t12 Type
t22  
eqType' (ForAllTy (Bndr TyVar
v1 ArgFlag
_) Type
t1) (ForAllTy (Bndr TyVar
v2 ArgFlag
_) Type
t2) 
  = Type -> Type -> Bool
eqType' Type
t1 (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
v2 (TyVar -> Type
TyVarTy TyVar
v1) Type
t2) 
eqType' (TyVarTy TyVar
v1) (TyVarTy TyVar
v2) 
  = TyVar
v1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
v2 
eqType' (AppTy Type
t11 Type
t12) (AppTy Type
t21 Type
t22) 
  = Type -> Type -> Bool
eqType' Type
t11 Type
t21 Bool -> Bool -> Bool
&& Type -> Type -> Bool
eqType' Type
t12 Type
t22  
eqType' (TyConApp TyCon
c1 [Type]
ts1) (TyConApp TyCon
c2 [Type]
ts2) 
  = TyCon
c1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
c2 Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Type -> Type -> Bool) -> [Type] -> [Type] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Bool
eqType' [Type]
ts1 [Type]
ts2) 
eqType' Type
_ Type
_ 
  = Bool
False 


deriving instance (Eq tyvar, Eq argf) => Eq (VarBndr tyvar argf)

instance Eq Coercion where
  Coercion
_ == :: Coercion -> Coercion -> Bool
== Coercion
_ = Bool
True 


showTy :: Type -> String 
showTy :: Type -> String
showTy (TyConApp TyCon
c [Type]
ts) = String
"(RApp   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TyCon -> String
forall a. Outputable a => a -> String
showPpr TyCon
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
sep' String
", " (Type -> String
showTy (Type -> String) -> [Type] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
showTy (AppTy Type
t1 Type
t2)   = String
"(TAppTy " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Type -> String
showTy Type
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showTy Type
t2) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" 
showTy (TyVarTy TyVar
v)   = String
"(RVar " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v)  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" 
showTy (ForAllTy (Bndr TyVar
v ArgFlag
_) Type
t)  = String
"ForAllTy " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". (" String -> String -> String
forall a. [a] -> [a] -> [a]
++  Type -> String
showTy Type
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
showTy (FunTy AnonArgFlag
af Type
t1 Type
t2) = String
"FunTy " String -> String -> String
forall a. [a] -> [a] -> [a]
++ AnonArgFlag -> String
forall a. Outputable a => a -> String
showPpr AnonArgFlag
af String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
showTy Type
t1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". (" String -> String -> String
forall a. [a] -> [a] -> [a]
++  Type -> String
showTy Type
t2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
showTy (CastTy Type
_ Coercion
_)    = String
"CastTy"
showTy (CoercionTy Coercion
_)  = String
"CoercionTy"
showTy (LitTy TyLit
_)       = String
"LitTy"

sep' :: String -> [String] -> String
sep' :: String -> [String] -> String
sep' String
_ [String
x] = String
x
sep' String
_ []  = []
sep' String
s (String
x:[String]
xs) = String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
sep' String
s [String]
xs 



-------------------------------------------------------------------------------
-- | GHC Type Substitutions ---------------------------------------------------
-------------------------------------------------------------------------------

class SubstTy a where
  subst :: TyVar -> Type -> a -> a
  subst TyVar
_ Type
_ = a -> a
forall a. a -> a
id  

instance SubstTy Type where
  subst :: TyVar -> Type -> Type -> Type
subst = TyVar -> Type -> Type -> Type
substType

substType :: TyVar -> Type -> Type -> Type
substType :: TyVar -> Type -> Type -> Type
substType TyVar
x Type
tx (TyConApp TyCon
c [Type]
ts) 
  = TyCon -> [Type] -> Type
TyConApp TyCon
c (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Type -> Type) -> [Type] -> [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
substType TyVar
x Type
tx (AppTy Type
t1 Type
t2)   
  = Type -> Type -> Type
AppTy (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2) 
substType TyVar
x Type
tx (TyVarTy TyVar
y)   
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y
  = Type
tx 
  | Bool
otherwise
  = TyVar -> Type
TyVarTy TyVar
y 
substType TyVar
x Type
tx (FunTy AnonArgFlag
aaf Type
t1 Type
t2)
  = AnonArgFlag -> Type -> Type -> Type
FunTy AnonArgFlag
aaf (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substType TyVar
x Type
tx f :: Type
f@(ForAllTy b :: TyVarBinder
b@(Bndr TyVar
y ArgFlag
_) Type
t)  
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y 
  = Type
f
  | Bool
otherwise 
  = TyVarBinder -> Type -> Type
ForAllTy TyVarBinder
b (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t)
substType TyVar
x Type
tx (CastTy Type
t Coercion
c)    
  = Type -> Coercion -> Type
CastTy (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substType TyVar
x Type
tx (CoercionTy Coercion
c)  
  = Coercion -> Type
CoercionTy (Coercion -> Type) -> Coercion -> Type
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c 
substType TyVar
_ Type
_  (LitTy TyLit
l)
  = TyLit -> Type
LitTy TyLit
l  


instance SubstTy Coercion where
  subst :: TyVar -> Type -> Coercion -> Coercion
subst = TyVar -> Type -> Coercion -> Coercion
substCoercion

substCoercion :: TyVar -> Type -> Coercion -> Coercion
substCoercion :: TyVar -> Type -> Coercion -> Coercion
substCoercion TyVar
x Type
tx (TyConAppCo Role
r TyCon
c [Coercion]
cs)
  = Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) TyCon
c (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)
substCoercion TyVar
x Type
tx (AppCo Coercion
c1 Coercion
c2)
  = Coercion -> Coercion -> Coercion
AppCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (FunCo Role
r Coercion
c1 Coercion
c2)
  = Role -> Coercion -> Coercion -> Coercion
FunCo Role
r (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (ForAllCo TyVar
y Coercion
c1 Coercion
c2)
  | TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
y 
  = (TyVar -> Coercion -> Coercion -> Coercion
ForAllCo TyVar
y Coercion
c1 Coercion
c2)
  | Bool
otherwise 
  = TyVar -> Coercion -> Coercion -> Coercion
ForAllCo TyVar
y (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
_ Type
_ (CoVarCo TyVar
y)
  = TyVar -> Coercion
CoVarCo TyVar
y 
substCoercion TyVar
x Type
tx (AxiomInstCo CoAxiom Branched
co BranchIndex
bi [Coercion]
cs)
  = CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
AxiomInstCo (TyVar -> Type -> CoAxiom Branched -> CoAxiom Branched
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiom Branched
co) BranchIndex
bi (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)  
substCoercion TyVar
x Type
tx (UnivCo UnivCoProvenance
y Role
r Type
t1 Type
t2)
  = UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo (TyVar -> Type -> UnivCoProvenance -> UnivCoProvenance
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx UnivCoProvenance
y) (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t1) (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t2)
substCoercion TyVar
x Type
tx (SymCo Coercion
c)
  = Coercion -> Coercion
SymCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (TransCo Coercion
c1 Coercion
c2)
  = Coercion -> Coercion -> Coercion
TransCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (AxiomRuleCo CoAxiomRule
ca [Coercion]
cs)
  = CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo (TyVar -> Type -> CoAxiomRule -> CoAxiomRule
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx CoAxiomRule
ca)  (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Coercion -> Coercion) -> [Coercion] -> [Coercion]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Coercion]
cs)  
substCoercion TyVar
x Type
tx (NthCo Role
r BranchIndex
i Coercion
c)
  = Role -> BranchIndex -> Coercion -> Coercion
NthCo Role
r BranchIndex
i (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (LRCo LeftOrRight
i Coercion
c)
  = LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
i (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (InstCo Coercion
c1 Coercion
c2)
  = Coercion -> Coercion -> Coercion
InstCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c1) (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c2)
substCoercion TyVar
x Type
tx (KindCo Coercion
c)
  = Coercion -> Coercion
KindCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
substCoercion TyVar
x Type
tx (SubCo Coercion
c)
  = Coercion -> Coercion
SubCo (TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c)
#ifdef MIN_VERSION_GLASGOW_HASKELL
#if MIN_VERSION_GLASGOW_HASKELL(8,6,5,0) && !MIN_VERSION_GLASGOW_HASKELL(8,8,1,0)
substCoercion x tx (Refl r t)
  = Refl (subst x tx r) (subst x tx t)
substCoercion x tx (CoherenceCo c1 c2)
  = CoherenceCo (subst x tx c1) (subst x tx c2)
#endif
#if MIN_VERSION_GLASGOW_HASKELL(8,10,0,0)
substCoercion TyVar
x Type
tx (Refl Type
t)
  = Type -> Coercion
Refl (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t)
substCoercion TyVar
x Type
tx (GRefl Role
r Type
t MCoercionN
co) -- FIXME(adn) Is this a correct substitution?
  = Role -> Type -> MCoercionN -> Coercion
GRefl Role
r (TyVar -> Type -> Type -> Type
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Type
t) MCoercionN
co     -- FIXME(adn) Is this a correct substitution?
substCoercion TyVar
_x Type
_tx (HoleCo CoercionHole
cH)
  = CoercionHole -> Coercion
HoleCo CoercionHole
cH                     -- FIXME(adn) Is this a correct substitution?
#endif
#endif

instance SubstTy Role where
instance SubstTy (CoAxiom Branched) where

instance SubstTy UnivCoProvenance where
  subst :: TyVar -> Type -> UnivCoProvenance -> UnivCoProvenance
subst TyVar
x Type
tx (PhantomProv Coercion
c)
    = Coercion -> UnivCoProvenance
PhantomProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c 
  subst TyVar
x Type
tx (ProofIrrelProv Coercion
c)
    = Coercion -> UnivCoProvenance
ProofIrrelProv (Coercion -> UnivCoProvenance) -> Coercion -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ TyVar -> Type -> Coercion -> Coercion
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Coercion
c 
  subst TyVar
_ Type
_ UnivCoProvenance
ch 
    = UnivCoProvenance
ch 

instance SubstTy CoAxiomRule where
  subst :: TyVar -> Type -> CoAxiomRule -> CoAxiomRule
subst TyVar
x Type
tx (CoAxiomRule FastString
n [Role]
rs Role
r [TypeEqn] -> Maybe TypeEqn
ps) 
    = FastString
-> [Role] -> Role -> ([TypeEqn] -> Maybe TypeEqn) -> CoAxiomRule
CoAxiomRule FastString
n (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (Role -> Role) -> [Role] -> [Role]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Role]
rs) (TyVar -> Type -> Role -> Role
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx Role
r) (\[TypeEqn]
eq -> TyVar -> Type -> Maybe TypeEqn -> Maybe TypeEqn
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx ([TypeEqn] -> Maybe TypeEqn
ps (TyVar -> Type -> [TypeEqn] -> [TypeEqn]
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx [TypeEqn]
eq)))

instance (SubstTy a, Functor m) => SubstTy (m a) where
  subst :: TyVar -> Type -> m a -> m a
subst TyVar
x Type
tx m a
xs = TyVar -> Type -> a -> a
forall a. SubstTy a => TyVar -> Type -> a -> a
subst TyVar
x Type
tx (a -> a) -> m a -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
xs