{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.LHS
( checkLeftHandSide
, LHSResult(..)
, bindAsPatterns
, IsFlexiblePattern(..)
, checkSortOfSplitVar
) where
#if MIN_VERSION_base(4,11,0)
import Prelude hiding ( (<>), mapM, null, sequence )
#else
import Prelude hiding ( mapM, null, sequence )
#endif
import Data.Maybe
import Control.Arrow (left)
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Trans.Maybe
import Data.Either (partitionEithers)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as List
import Data.Monoid ( Monoid, mempty, mappend )
import Data.Semigroup ( Semigroup )
import qualified Data.Semigroup as Semigroup
import qualified Data.Map as Map
import Agda.Interaction.Highlighting.Generate (storeDisambiguatedName)
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView, deepUnscope)
import Agda.Syntax.Common as Common
import Agda.Syntax.Info as A
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin (litType, constructorForm)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.CheckInternal (checkInternal)
import Agda.TypeChecking.Datatypes hiding (isDataOrRecordType)
import Agda.TypeChecking.Errors (dropTopLevelModule)
import Agda.TypeChecking.Irrelevance
import {-# SOURCE #-} Agda.TypeChecking.Empty
import Agda.TypeChecking.Forcing
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records hiding (getRecordConstructor)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import {-# SOURCE #-} Agda.TypeChecking.Rules.Term (checkExpr)
import Agda.TypeChecking.Rules.LHS.Problem
import Agda.TypeChecking.Rules.LHS.ProblemRest
import Agda.TypeChecking.Rules.LHS.Unify
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.Data
import Agda.Utils.Except (MonadError(..), ExceptT, runExceptT)
import Agda.Utils.Function
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.NonemptyList
import Agda.Utils.Null
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Singleton
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
flexiblePatterns :: [NamedArg A.Pattern] -> TCM FlexibleVars
flexiblePatterns nps = do
forMaybeM (zip (downFrom $ length nps) nps) $ \ (i, Arg ai p) -> do
runMaybeT $ (\ f -> FlexibleVar (getHiding ai) (getOrigin ai) f (Just i) i) <$> maybeFlexiblePattern p
class IsFlexiblePattern a where
maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind
isFlexiblePattern :: a -> TCM Bool
isFlexiblePattern p =
maybe False notOtherFlex <$> runMaybeT (maybeFlexiblePattern p)
where
notOtherFlex = \case
RecordFlex fls -> all notOtherFlex fls
ImplicitFlex -> True
DotFlex -> True
OtherFlex -> False
instance IsFlexiblePattern A.Pattern where
maybeFlexiblePattern p = do
reportSDoc "tc.lhs.flex" 30 $ text "maybeFlexiblePattern" <+> prettyA p
reportSDoc "tc.lhs.flex" 60 $ text "maybeFlexiblePattern (raw) " <+> (text . show . deepUnscope) p
case p of
A.DotP{} -> return DotFlex
A.VarP{} -> return ImplicitFlex
A.WildP{} -> return ImplicitFlex
A.AsP _ _ p -> maybeFlexiblePattern p
A.ConP _ cs qs | Just c <- getUnambiguous cs ->
ifM (isNothing <$> isRecordConstructor c) (return OtherFlex)
(maybeFlexiblePattern qs)
A.LitP{} -> return OtherFlex
_ -> mzero
instance IsFlexiblePattern (I.Pattern' a) where
maybeFlexiblePattern p =
case p of
I.DotP{} -> return DotFlex
I.ConP _ i ps
| Just PatOSystem <- conPRecord i -> return ImplicitFlex
| Just _ <- conPRecord i -> maybeFlexiblePattern ps
| otherwise -> mzero
I.VarP{} -> mzero
I.LitP{} -> mzero
I.ProjP{} -> mzero
instance IsFlexiblePattern a => IsFlexiblePattern [a] where
maybeFlexiblePattern ps = RecordFlex <$> mapM maybeFlexiblePattern ps
instance IsFlexiblePattern a => IsFlexiblePattern (Arg a) where
maybeFlexiblePattern = maybeFlexiblePattern . unArg
instance IsFlexiblePattern a => IsFlexiblePattern (Common.Named name a) where
maybeFlexiblePattern = maybeFlexiblePattern . namedThing
updateProblemEqs
:: [ProblemEq] -> TCM [ProblemEq]
updateProblemEqs eqs = do
reportSDoc "tc.lhs.top" 20 $ vcat
[ text "updateProblem: equations to update"
, nest 2 (vcat $ map prettyTCM eqs)
]
eqs' <- updates eqs
reportSDoc "tc.lhs.top" 20 $ vcat
[ text "updateProblem: new equations"
, nest 2 (vcat $ map prettyTCM eqs')
]
return eqs'
where
updates :: [ProblemEq] -> TCM [ProblemEq]
updates = concat <.> traverse update
update :: ProblemEq -> TCM [ProblemEq]
update eq@(ProblemEq A.WildP{} _ _) = return []
update eq@(ProblemEq p v a) = reduce v >>= constructorForm >>= \case
Con c ci es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
contype <- getFullyAppliedConType c =<< reduce (unDom a)
caseMaybe contype (return [eq]) $ \((d,_,pars),b) -> do
TelV ctel _ <- telView b
let bs = instTel ctel (map unArg vs)
p <- expandLitPattern p
case p of
A.AsP info x p' ->
(ProblemEq (A.VarP x) v a :) <$> update (ProblemEq p' v a)
A.ConP cpi ambC ps -> do
(c',_) <- disambiguateConstructor ambC d pars
if conName c /= conName c' then return [eq] else do
ps <- insertImplicitPatterns ExpandLast ps ctel
reportSDoc "tc.lhs.imp" 20 $
text "insertImplicitPatternsT returned" <+> fsep (map prettyA ps)
let checkArgs [] [] = return ()
checkArgs (p : ps) (v : vs)
| getHiding p == getHiding v = checkArgs ps vs
| otherwise = setCurrentRange p $ genericDocError =<< do
fsep $ pwords ("Expected an " ++ which (getHiding v) ++ " argument " ++
"instead of " ++ which (getHiding p) ++ " argument") ++
[ prettyA p ]
where which NotHidden = "explicit"
which Hidden = "implicit"
which Instance{} = "instance"
checkArgs [] vs = genericDocError =<< do
fsep $ pwords "Too few arguments to constructor" ++ [prettyTCM c <> text ","] ++
pwords ("expected " ++ show n ++ " more explicit " ++ arguments)
where n = length (filter visible vs)
arguments | n == 1 = "argument"
| otherwise = "arguments"
checkArgs (p : _) [] = setCurrentRange p $ genericDocError =<< do
fsep $ pwords "Too many arguments to constructor" ++ [prettyTCM c]
checkArgs ps vs
updates $ zipWith3 ProblemEq (map namedArg ps) (map unArg vs) bs
A.RecP pi fs -> do
axs <- recordFieldNames . theDef <$> getConstInfo d
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs axs
ps <- insertImplicitPatterns ExpandLast ps ctel
let eqs = zipWith3 ProblemEq (map namedArg ps) (map unArg vs) bs
updates eqs
_ -> return [eq]
Lit l | A.LitP l' <- p , l == l' -> return []
_ -> return [eq]
instTel :: Telescope -> [Term] -> [Dom Type]
instTel EmptyTel _ = []
instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
instTel ExtendTel{} [] = __IMPOSSIBLE__
isSolvedProblem :: Problem a -> Bool
isSolvedProblem problem = null (problem ^. problemRestPats) &&
problemAllVariables problem
problemAllVariables :: Problem a -> Bool
problemAllVariables problem =
all (isSolved . snd . asView) $
map namedArg (problem ^. problemRestPats) ++ problemInPats problem
where
isSolved A.ConP{} = False
isSolved A.LitP{} = False
isSolved A.RecP{} = False
isSolved A.VarP{} = True
isSolved A.WildP{} = True
isSolved A.DotP{} = True
isSolved A.AbsurdP{} = True
isSolved A.ProjP{} = __IMPOSSIBLE__
isSolved A.DefP{} = __IMPOSSIBLE__
isSolved A.AsP{} = __IMPOSSIBLE__
isSolved A.PatternSynP{} = __IMPOSSIBLE__
isSolved A.WithP{} = __IMPOSSIBLE__
noShadowingOfConstructors
:: Call
-> [ProblemEq] -> TCM ()
noShadowingOfConstructors mkCall eqs =
traceCall mkCall $ mapM_ noShadowing eqs
where
noShadowing (ProblemEq p _ (Dom info (El _ a))) = case snd $ asView p of
A.WildP {} -> return ()
A.AbsurdP {} -> return ()
A.DotP {} -> return ()
A.ConP {} -> __IMPOSSIBLE__
A.RecP {} -> __IMPOSSIBLE__
A.ProjP {} -> __IMPOSSIBLE__
A.DefP {} -> __IMPOSSIBLE__
A.AsP {} -> __IMPOSSIBLE__
A.LitP {} -> __IMPOSSIBLE__
A.PatternSynP {} -> __IMPOSSIBLE__
A.WithP {} -> __IMPOSSIBLE__
A.VarP (A.BindName x) -> when (getOrigin info == UserWritten) $ do
reportSDoc "tc.lhs.shadow" 30 $ vcat
[ text $ "checking whether pattern variable " ++ prettyShow x ++ " shadows a constructor"
, nest 2 $ text "type of variable =" <+> prettyTCM a
, nest 2 $ text "position of variable =" <+> (text . show) (getRange x)
]
reportSDoc "tc.lhs.shadow" 70 $ nest 2 $ text "a =" <+> pretty a
a <- reduce a
case a of
Def t _ -> do
d <- theDef <$> getConstInfo t
case d of
Datatype { dataCons = cs } -> do
case filter ((A.nameConcrete x ==) . A.nameConcrete . A.qnameName) cs of
[] -> return ()
(c : _) -> setCurrentRange x $
typeError $ PatternShadowsConstructor x c
AbstractDefn{} -> return ()
Axiom {} -> return ()
Function {} -> return ()
Record {} -> return ()
Constructor {} -> __IMPOSSIBLE__
Primitive {} -> return ()
Var {} -> return ()
Pi {} -> return ()
Sort {} -> return ()
MetaV {} -> return ()
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
checkDotPattern :: DotPattern -> TCM ()
checkDotPattern (Dot e v (Dom info a)) =
traceCall (CheckDotPattern e v) $ do
reportSDoc "tc.lhs.dot" 15 $
sep [ text "checking dot pattern"
, nest 2 $ prettyA e
, nest 2 $ text "=" <+> prettyTCM v
, nest 2 $ text ":" <+> prettyTCM a
]
applyRelevanceToContext (getRelevance info) $ do
u <- checkExpr e a
reportSDoc "tc.lhs.dot" 50 $
sep [ text "equalTerm"
, nest 2 $ pretty a
, nest 2 $ pretty u
, nest 2 $ pretty v
]
noConstraints $ equalTerm a u v
checkAbsurdPattern :: AbsurdPattern -> TCM ()
checkAbsurdPattern (Absurd r a) = isEmptyType r a
data LeftoverPatterns = LeftoverPatterns
{ patternVariables :: IntMap [A.Name]
, asPatterns :: [AsBinding]
, dotPatterns :: [DotPattern]
, absurdPatterns :: [AbsurdPattern]
}
instance Semigroup LeftoverPatterns where
x <> y = LeftoverPatterns
{ patternVariables = IntMap.unionWith (++) (patternVariables x) (patternVariables y)
, asPatterns = asPatterns x ++ asPatterns y
, dotPatterns = dotPatterns x ++ dotPatterns y
, absurdPatterns = absurdPatterns x ++ absurdPatterns y
}
instance Monoid LeftoverPatterns where
mempty = LeftoverPatterns empty [] [] []
mappend = (Semigroup.<>)
getLeftoverPatterns :: [ProblemEq] -> TCM LeftoverPatterns
getLeftoverPatterns eqs = do
reportSDoc "tc.lhs.top" 30 $ text "classifying leftover patterns"
mconcat <$> mapM getLeftoverPattern eqs
where
patternVariable x i = LeftoverPatterns (singleton (i,[x])) [] [] []
asPattern x v a = LeftoverPatterns empty [AsB x v (unDom a)] [] []
dotPattern e v a = LeftoverPatterns empty [] [Dot e v a] []
absurdPattern info a = LeftoverPatterns empty [] [] [Absurd info a]
getLeftoverPattern :: ProblemEq -> TCM LeftoverPatterns
getLeftoverPattern (ProblemEq p v a) = case p of
(A.VarP (A.BindName x)) -> isEtaVar v (unDom a) >>= \case
Just i -> return $ patternVariable x i
Nothing -> return $ asPattern x v a
(A.WildP _) -> return mempty
(A.AsP info (A.BindName x) p) -> (asPattern x v a `mappend`) <$> do
getLeftoverPattern $ ProblemEq p v a
(A.DotP info e) -> return $ dotPattern e v a
(A.AbsurdP info) -> return $ absurdPattern (getRange info) (unDom a)
A.ConP{} -> __IMPOSSIBLE__
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.LitP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.RecP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
getUserVariableNames :: Telescope -> IntMap [A.Name]
-> ([Maybe A.Name], [AsBinding])
getUserVariableNames tel names = runWriter $
zipWithM makeVar (flattenTel tel) (downFrom $ size tel)
where
makeVar :: Dom Type -> Int -> Writer [AsBinding] (Maybe A.Name)
makeVar a i | Just (x:xs) <- IntMap.lookup i names = do
tell $ map (\y -> AsB y (var i) (unDom a)) xs
return $ Just x
makeVar a i = return Nothing
transferOrigins :: [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> TCM [NamedArg DeBruijnPattern]
transferOrigins ps qs = do
reportSDoc "tc.lhs.origin" 40 $ vcat
[ text "transferOrigins"
, nest 2 $ vcat
[ text "ps = " <+> prettyA ps
, text "qs = " <+> pretty qs
]
]
transfers ps qs
where
transfers :: [NamedArg A.Pattern]
-> [NamedArg DeBruijnPattern]
-> TCM [NamedArg DeBruijnPattern]
transfers [] qs
| all notVisible qs = return $ map (setOrigin Inserted) qs
| otherwise = __IMPOSSIBLE__
transfers (p : ps) [] = __IMPOSSIBLE__
transfers (p : ps) (q : qs)
| matchingArgs p q = do
q' <- setOrigin (getOrigin p) <$>
(traverse $ traverse $ transfer $ namedArg p) q
(q' :) <$> transfers ps qs
| otherwise = (setOrigin Inserted q :) <$> transfers (p : ps) qs
transfer :: A.Pattern -> DeBruijnPattern -> TCM DeBruijnPattern
transfer p q = case (snd (asView p) , q) of
(A.ConP pi _ ps , ConP c (ConPatternInfo mo mb l) qs) -> do
let cpi = ConPatternInfo (mo $> PatOCon) mb l
ConP c cpi <$> transfers ps qs
(A.RecP pi fs , ConP c (ConPatternInfo mo mb l) qs) -> do
let Def d _ = unEl $ unArg $ fromMaybe __IMPOSSIBLE__ mb
axs = map (nameConcrete . qnameName) (conFields c) `withArgsFrom` qs
cpi = ConPatternInfo (mo $> PatORec) mb l
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs axs
ConP c cpi <$> transfers ps qs
(p , ConP c (ConPatternInfo mo mb l) qs) -> do
let cpi = ConPatternInfo (mo $> patOrigin p) mb l
return $ ConP c cpi qs
(p , VarP _ x) -> return $ VarP (patOrigin p) x
(p , DotP _ u) -> return $ DotP (patOrigin p) u
_ -> return q
patOrigin :: A.Pattern -> PatOrigin
patOrigin (A.VarP (A.BindName x)) = PatOVar x
patOrigin A.DotP{} = PatODot
patOrigin A.ConP{} = PatOCon
patOrigin A.RecP{} = PatORec
patOrigin A.WildP{} = PatOWild
patOrigin A.AbsurdP{} = PatOAbsurd
patOrigin A.LitP{} = PatOLit
patOrigin A.AsP{} = __IMPOSSIBLE__
patOrigin A.ProjP{} = __IMPOSSIBLE__
patOrigin A.DefP{} = __IMPOSSIBLE__
patOrigin A.PatternSynP{} = __IMPOSSIBLE__
patOrigin A.WithP{} = __IMPOSSIBLE__
matchingArgs :: NamedArg A.Pattern -> NamedArg DeBruijnPattern -> Bool
matchingArgs p q
| isJust (A.maybePostfixProjP p) = isJust (isProjP q)
| visible p && visible q = True
| sameHiding p q && isNothing (nameOf (unArg p)) = True
| sameHiding p q && nameOf (unArg p) == nameOf (unArg q) = True
| otherwise = False
checkPatternLinearity :: [ProblemEq] -> TCM [ProblemEq]
checkPatternLinearity eqs = do
reportSDoc "tc.lhs.top" 30 $ text "Checking linearity of pattern variables"
check Map.empty eqs
where
check _ [] = return []
check vars (eq@(ProblemEq p u a) : eqs) = case p of
A.VarP x | Just v <- Map.lookup x vars -> do
noConstraints $ equalTerm (unDom a) u v
check vars eqs
A.VarP x | otherwise -> (eq:) <$> do
check (Map.insert x u vars) eqs
A.AsP _ x p ->
check vars $ [ProblemEq (A.VarP x) u a, ProblemEq p u a] ++ eqs
A.WildP{} -> continue
A.DotP{} -> continue
A.AbsurdP{} -> continue
A.ConP{} -> __IMPOSSIBLE__
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.LitP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.RecP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
where continue = (eq:) <$> check vars eqs
computeLHSContext :: [Maybe A.Name] -> Telescope -> TCM Context
computeLHSContext = go [] []
where
go cxt _ [] tel@ExtendTel{} = do
reportSDoc "impossible" 10 $
text "computeLHSContext: no patterns left, but tel =" <+> prettyTCM tel
__IMPOSSIBLE__
go cxt _ (_ : _) EmptyTel = __IMPOSSIBLE__
go cxt _ [] EmptyTel = return cxt
go cxt taken (x : xs) tel0@(ExtendTel a tel) = do
name <- maybe (dummyName taken $ absName tel) return x
let e = (name,) <$> a
go (e : cxt) (name : taken) xs (absBody tel)
dummyName taken s =
if isUnderscore s then freshNoName_
else unshadowedName taken <$> freshName_ ("." ++ argNameToString s)
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
bindAsPatterns [] ret = ret
bindAsPatterns (AsB x v a : asb) ret = do
reportSDoc "tc.lhs.as" 10 $ text "as pattern" <+> prettyTCM x <+>
sep [ text ":" <+> prettyTCM a
, text "=" <+> prettyTCM v
]
addLetBinding defaultArgInfo x v a $ bindAsPatterns asb ret
recheckStrippedWithPattern :: ProblemEq -> TCM ()
recheckStrippedWithPattern (ProblemEq p v a) = checkInternal v (unDom a)
`catchError` \_ -> typeError . GenericDocError =<< vcat
[ text "Ill-typed pattern after with abstraction: " <+> prettyA p
, text "(perhaps you can replace it by `_`?)"
]
data LHSResult = LHSResult
{ lhsParameters :: Nat
, lhsVarTele :: Telescope
, lhsPatterns :: [NamedArg DeBruijnPattern]
, lhsHasAbsurd :: Bool
, lhsBodyType :: Arg Type
, lhsPatSubst :: Substitution
, lhsAsBindings :: [AsBinding]
}
instance InstantiateFull LHSResult where
instantiateFull' (LHSResult n tel ps abs t sub as) = LHSResult n
<$> instantiateFull' tel
<*> instantiateFull' ps
<*> instantiateFull' abs
<*> instantiateFull' t
<*> instantiateFull' sub
<*> instantiateFull' as
checkLeftHandSide :: forall a.
Call
-> Maybe QName
-> [NamedArg A.Pattern]
-> Type
-> Maybe Substitution
-> [ProblemEq]
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide c f ps a withSub' strippedPats = Bench.billToCPS [Bench.Typing, Bench.CheckLHS] $ \ ret -> do
cxt <- map (setOrigin Inserted) . reverse <$> getContext
let tel = telFromList' prettyShow cxt
cps = [ unnamed . A.VarP . A.BindName . fst <$> argFromDom d
| d <- cxt ]
eqs0 = zipWith3 ProblemEq (map namedArg cps) (map var $ downFrom $ size tel) (flattenTel tel)
let finalChecks :: LHSState a -> TCM a
finalChecks (LHSState delta qs0 (Problem eqs rps _) b) = do
unless (null rps) __IMPOSSIBLE__
delta <- forceTranslateTelescope delta qs0
addContext delta $ do
noShadowingOfConstructors c eqs
noPatternMatchingOnCodata qs0
let notProj ProjP{} = False
notProj _ = True
numPats = length $ takeWhile (notProj . namedArg) qs0
weakSub :: Substitution
weakSub | isJust withSub' = wkS (max 0 $ numPats - arity a) idS
| otherwise = wkS (numPats - length cxt) idS
withSub = fromMaybe idS withSub'
patSub = (map (patternToTerm . namedArg) $ reverse $ take numPats qs0) ++# (EmptyS __IMPOSSIBLE__)
paramSub = patSub `composeS` weakSub `composeS` withSub
eqs <- addContext delta $ checkPatternLinearity eqs
LeftoverPatterns patVars asb0 dots absurds
<- addContext delta $ getLeftoverPatterns eqs
let (vars, asb1) = getUserVariableNames delta patVars
asb = asb0 ++ asb1
let makeVar = maybe deBruijnVar $ debruijnNamedVar . nameToArgName
ren = parallelS $ zipWith makeVar (reverse vars) [0..]
qs <- transferOrigins (cps ++ ps) $ applySubst ren qs0
let hasAbsurd = not . null $ absurds
let lhsResult = LHSResult (length cxt) delta qs hasAbsurd b patSub asb
reportSDoc "tc.lhs.top" 10 $
vcat [ text "checked lhs:"
, nest 2 $ vcat
[ text "delta = " <+> prettyTCM delta
, text "dots = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM dots)
, text "asb = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM asb)
, text "absurds = " <+> addContext delta (brackets $ fsep $ punctuate comma $ map prettyTCM absurds)
, text "qs = " <+> addContext delta (prettyList $ map pretty qs)
]
]
reportSDoc "tc.lhs.top" 30 $
nest 2 $ vcat
[ text "vars = " <+> text (show vars)
]
reportSDoc "tc.lhs.top" 20 $ nest 2 $ text "withSub = " <+> pretty withSub
reportSDoc "tc.lhs.top" 20 $ nest 2 $ text "weakSub = " <+> pretty weakSub
reportSDoc "tc.lhs.top" 20 $ nest 2 $ text "patSub = " <+> pretty patSub
reportSDoc "tc.lhs.top" 20 $ nest 2 $ text "paramSub = " <+> pretty paramSub
newCxt <- computeLHSContext vars delta
updateContext paramSub (const newCxt)
$ applyRelevanceToContext (getRelevance b) $ do
reportSDoc "tc.lhs.top" 10 $ text "bound pattern variables"
reportSDoc "tc.lhs.top" 60 $ nest 2 $ text "context = " <+> (pretty =<< getContextTelescope)
reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type = " <+> prettyTCM b
reportSDoc "tc.lhs.top" 60 $ nest 2 $ text "type = " <+> pretty b
bindAsPatterns asb $ do
mapM_ checkDotPattern dots
mapM_ checkAbsurdPattern absurds
ret lhsResult
st0 <- initLHSState tel eqs0 ps a finalChecks
let withSub = fromMaybe __IMPOSSIBLE__ withSub'
withEqs <- updateProblemEqs $ applySubst withSub strippedPats
inTopContext $ addContext (st0 ^. lhsTel) $
forM_ withEqs recheckStrippedWithPattern
let st = over (lhsProblem . problemEqs) (++ withEqs) st0
(result, block) <- inTopContext $ runWriterT $ checkLHS f st
return result
splitStrategy :: [ProblemEq] -> [ProblemEq]
splitStrategy = filter shouldSplit
where
shouldSplit :: ProblemEq -> Bool
shouldSplit (ProblemEq p v a) = case snd $ asView p of
A.LitP{} -> True
A.RecP{} -> True
A.ConP{} -> True
A.VarP{} -> False
A.WildP{} -> False
A.DotP{} -> False
A.AbsurdP{} -> False
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
checkLHS
:: forall tcm a. (MonadTCM tcm, MonadWriter Blocked_ tcm, HasConstInfo tcm, MonadError TCErr tcm, MonadDebug tcm)
=> Maybe QName
-> LHSState a
-> tcm a
checkLHS mf st@(LHSState tel ip problem target) = do
if isSolvedProblem problem then
liftTCM $ (problem ^. problemCont) st
else do
unlessM (optPatternMatching <$> gets getPragmaOptions) $
unless (problemAllVariables problem) $
typeError $ GenericError $ "Pattern matching is disabled"
let splitsToTry = splitStrategy $ problem ^. problemEqs
foldr trySplit trySplitRest splitsToTry >>= \case
Right st' -> do
let rel = getRelevance $ st' ^. lhsTarget
applyRelevanceToContext rel $ checkLHS mf st'
Left (err:_) -> throwError err
Left [] -> __IMPOSSIBLE__
where
trySplit :: ProblemEq
-> tcm (Either [TCErr] (LHSState a))
-> tcm (Either [TCErr] (LHSState a))
trySplit eq tryNextSplit = runExceptT (splitArg eq) >>= \case
Right st' -> return $ Right st'
Left err -> left (err:) <$> tryNextSplit
trySplitRest :: tcm (Either [TCErr] (LHSState a))
trySplitRest = case problem ^. problemRestPats of
[] -> return $ Left []
(p:_) -> left singleton <$> runExceptT (splitRest p)
splitArg :: ProblemEq -> ExceptT TCErr tcm (LHSState a)
splitArg (ProblemEq p v (Dom _ a)) = traceCall (CheckPattern p tel a) $ do
reportSDoc "tc.lhs.split" 30 $ sep
[ text "split looking at pattern"
, nest 2 $ text "p =" <+> prettyA p
]
i <- liftTCM $ addContext tel $ ifJustM (isEtaVar v a) return $
softTypeError $ SplitOnNonVariable v a
let pos = size tel - (i+1)
(delta1, tel'@(ExtendTel dom adelta2)) = splitTelescopeAt pos tel
p <- liftTCM $ expandLitPattern p
case snd $ asView p of
(A.LitP l) -> splitLit delta1 dom adelta2 l
p@A.RecP{} -> splitCon delta1 dom adelta2 p Nothing
p@(A.ConP _ c ps) -> splitCon delta1 dom adelta2 p $ Just c
A.VarP{} -> __IMPOSSIBLE__
A.WildP{} -> __IMPOSSIBLE__
A.DotP{} -> __IMPOSSIBLE__
A.AbsurdP{} -> __IMPOSSIBLE__
A.ProjP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
A.WithP{} -> __IMPOSSIBLE__
splitRest :: NamedArg A.Pattern -> ExceptT TCErr tcm (LHSState a)
splitRest p = setCurrentRange p $ do
reportSDoc "tc.lhs.split" 20 $ sep
[ text "splitting problem rest"
, nest 2 $ text "projection pattern =" <+> prettyA p
, nest 2 $ text "eliminates type =" <+> prettyTCM target
]
reportSDoc "tc.lhs.split" 80 $ sep
[ nest 2 $ text $ "projection pattern (raw) = " ++ show p
]
(orig, ambProjName) <- ifJust (A.maybePostfixProjP p) return $
addContext tel $ softTypeError $ CannotEliminateWithPattern p (unArg target)
(projName, projType) <- suspendErrors $
addContext tel $ disambiguateProjection (getHiding p) ambProjName target
f <- ifJust mf return $ hardTypeError $
GenericError "Cannot use copatterns in a let binding"
let self = Def f $ patternsToElims ip
target' <- traverse (`piApply1` self) projType
let projP = target' $> Named Nothing (ProjP orig projName)
ip' = ip ++ [projP]
problem' = over problemRestPats tail problem
liftTCM $ updateProblemRest (LHSState tel ip' problem' target')
splitLit :: Telescope
-> Dom Type
-> Abs Telescope
-> Literal
-> ExceptT TCErr tcm (LHSState a)
splitLit delta1 dom@(Dom info a) adelta2 lit = do
let delta2 = absApp adelta2 (Lit lit)
delta' = abstract delta1 delta2
rho = singletonS (size delta2) (LitP lit)
eqs' = applyPatSubst rho $ problem ^. problemEqs
ip' = applySubst rho ip
target' = applyPatSubst rho target
when (unusableRelevance $ getRelevance info) $
addContext delta1 $ hardTypeError $ SplitOnIrrelevant dom
suspendErrors $ equalType a =<< litType lit
eqs' <- liftTCM $ addContext delta' $ updateProblemEqs eqs'
let problem' = set problemEqs eqs' problem
liftTCM $ updateProblemRest (LHSState delta' ip' problem' target')
splitCon :: Telescope
-> Dom Type
-> Abs Telescope
-> A.Pattern
-> Maybe AmbiguousQName
-> ExceptT TCErr tcm (LHSState a)
splitCon delta1 dom@(Dom info a) adelta2 focusPat ambC = do
let delta2 = absBody adelta2
reportSDoc "tc.lhs.split" 10 $ vcat
[ text "checking lhs"
, nest 2 $ text "tel =" <+> prettyTCM tel
, nest 2 $ text "rel =" <+> (text $ show $ getRelevance info)
]
reportSDoc "tc.lhs.split" 15 $ vcat
[ text "split problem"
, nest 2 $ vcat
[ text "delta1 = " <+> prettyTCM delta1
, text "a = " <+> addContext delta1 (prettyTCM a)
, text "delta2 = " <+> addContext delta1 (addContext ("x", dom) (prettyTCM delta2))
]
]
(d, pars, ixs) <- addContext delta1 $ isDataOrRecordType dom
checkSortOfSplitVar a
(c, b) <- liftTCM $ addContext delta1 $ case ambC of
Just ambC -> disambiguateConstructor ambC d pars
Nothing -> getRecordConstructor d pars a
case focusPat of
A.ConP cpi _ _ | patLazy cpi -> softTypeError $
ForcedConstructorNotInstantiated focusPat
_ -> return ()
TelV gamma (El _ ctarget) <- liftTCM $ telView b
let Def d' es' = ctarget
cixs = drop (size pars) $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es'
unless (d == d') __IMPOSSIBLE__
gamma <- liftTCM $ case focusPat of
A.ConP _ _ ps -> do
ps <- insertImplicitPatterns ExpandLast ps gamma
return $ useNamesFromPattern ps gamma
A.RecP _ fs -> do
axs <- recordFieldNames . theDef <$> getConstInfo d
ps <- insertMissingFields d (const $ A.WildP patNoRange) fs axs
ps <- insertImplicitPatterns ExpandLast ps gamma
return $ useNamesFromPattern ps gamma
_ -> __IMPOSSIBLE__
let updRel = composeRelevance (getRelevance info)
gamma <- return $ mapRelevance updRel <$> gamma
da <- (`piApply` pars) . defType <$> getConstInfo d
reportSDoc "tc.lhs.split" 30 $ text " da = " <+> prettyTCM da
reportSDoc "tc.lhs.top" 15 $ addContext delta1 $
sep [ text "preparing to unify"
, nest 2 $ vcat
[ text "c =" <+> prettyTCM c <+> text ":" <+> prettyTCM b
, text "d =" <+> prettyTCM (Def d (map Apply pars)) <+> text ":" <+> prettyTCM da
, text "gamma =" <+> prettyTCM gamma
, text "pars =" <+> brackets (fsep $ punctuate comma $ map prettyTCM pars)
, text "ixs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ixs)
, text "cixs =" <+> addContext gamma (brackets (fsep $ punctuate comma $ map prettyTCM cixs))
]
]
let delta1Gamma = delta1 `abstract` gamma
da' = raise (size gamma) da
ixs' = raise (size gamma) ixs
let flex = allFlexVars $ delta1Gamma
liftTCM (unifyIndices delta1Gamma flex da' cixs ixs') >>= \case
NoUnify neg -> hardTypeError $ ImpossibleConstructor (conName c) neg
DontKnow errs -> softTypeError $ SplitError $
UnificationStuck (conName c) (delta1 `abstract` gamma) cixs ixs' errs
Unifies (delta1',rho0,es) -> do
reportSDoc "tc.lhs.top" 15 $ text "unification successful"
reportSDoc "tc.lhs.top" 20 $ nest 2 $ vcat
[ text "delta1' =" <+> prettyTCM delta1'
, text "rho0 =" <+> addContext delta1' (prettyTCM rho0)
, text "es =" <+> addContext delta1' (prettyTCM $ (fmap . fmap . fmap) patternToTerm es)
]
let (rho1,rho2) = splitS (size gamma) rho0
reportSDoc "tc.lhs.top" 20 $ addContext delta1' $ nest 2 $ vcat
[ text "rho1 =" <+> prettyTCM rho1
, text "rho2 =" <+> prettyTCM rho2
]
let a' = applyPatSubst rho1 a
isRec <- isRecord d
let cpi = ConPatternInfo { conPRecord = isRec $> PatOCon
, conPType = Just $ Arg info a'
, conPLazy = False }
let crho2 = ConP c cpi $ applySubst rho2 $ teleNamedArgs gamma
rho3 = consS crho2 rho1
delta2' = applyPatSubst rho3 delta2
delta' = delta1' `abstract` delta2'
rho = liftS (size delta2) rho3
reportSDoc "tc.lhs.top" 20 $ addContext delta1' $ nest 2 $ vcat
[ text "crho2 =" <+> prettyTCM crho2
, text "rho3 =" <+> prettyTCM rho3
, text "delta2' =" <+> prettyTCM delta2'
]
reportSDoc "tc.lhs.top" 70 $ addContext delta1' $ nest 2 $ vcat
[ text "crho2 =" <+> pretty crho2
, text "rho3 =" <+> pretty rho3
, text "delta2' =" <+> pretty delta2'
]
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "delta' =" <+> prettyTCM delta'
, text "rho =" <+> addContext delta' (prettyTCM rho)
]
let ip' = applySubst rho ip
target' = applyPatSubst rho target
let eqs' = applyPatSubst rho $ problem ^. problemEqs
eqs' <- liftTCM $ addContext delta' $ updateProblemEqs eqs'
let problem' = set problemEqs eqs' problem
st' <- liftTCM $ updateProblemRest $ LHSState delta' ip' problem' target'
reportSDoc "tc.lhs.top" 12 $ sep
[ text "new problem from rest"
, nest 2 $ vcat
[ text "delta' =" <+> prettyTCM (st' ^. lhsTel)
, text "eqs' =" <+> addContext (st' ^. lhsTel) (prettyTCM $ st' ^. lhsProblem ^. problemEqs)
, text "ip' =" <+> addContext (st' ^. lhsTel) (pretty $ st' ^. lhsOutPat)
]
]
return st'
noPatternMatchingOnCodata :: [NamedArg DeBruijnPattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . namedArg)
where
check (VarP {}) = return ()
check (DotP {}) = return ()
check (ProjP{}) = return ()
check (LitP {}) = return ()
check (ConP con _ ps) = do
reportSDoc "tc.lhs.top" 40 $
text "checking whether" <+> prettyTCM con <+> text "is a coinductive constructor"
TelV _ t <- telView' . defType <$> do getConstInfo $ conName con
c <- isCoinductive t
case c of
Nothing -> __IMPOSSIBLE__
Just False -> mapM_ (check . namedArg) ps
Just True -> typeError $
GenericError "Pattern matching on coinductive types is not allowed"
suspendErrors :: (MonadTCM m, MonadError TCErr m) => TCM a -> m a
suspendErrors f = do
ok <- liftTCM $ (Right <$> f) `catchError` (return . Left)
either throwError return ok
softTypeError :: (MonadTCM m, MonadError TCErr m) => TypeError -> m a
softTypeError err = throwError =<< typeError_ err
hardTypeError :: (MonadTCM m) => TypeError -> m a
hardTypeError = liftTCM . typeError
isDataOrRecordType :: (MonadTCM m, MonadDebug m)
=> Dom Type -> ExceptT TCErr m (QName, Args, Args)
isDataOrRecordType dom@(Dom info a) = liftTCM (reduceB a) >>= \case
NotBlocked ReallyNotBlocked a -> case unEl a of
Def d es -> (liftTCM $ theDef <$> getConstInfo d) >>= \case
Datatype{dataPars = np} -> do
reportSLn "tc.lhs.split" 30 $ "split ConP: relevance is " ++ show (getRelevance info)
when (unusableRelevance $ getRelevance info) $
unlessM (liftTCM $ optExperimentalIrrelevance <$> pragmaOptions) $
hardTypeError $ SplitOnIrrelevant dom
let (pars, ixs) = splitAt np $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es
return (d, pars, ixs)
Record{} -> do
let pars = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
return (d, pars, [])
AbstractDefn{} -> hardTypeError . GenericDocError =<< do
liftTCM $ text "Cannot split on abstract data type" <+> prettyTCM d
Axiom{} -> hardTypeError =<< notData
Function{} -> hardTypeError =<< notData
Constructor{} -> __IMPOSSIBLE__
Primitive{} -> __IMPOSSIBLE__
Var{} -> softTypeError =<< notData
MetaV{} -> softTypeError =<< notData
Pi{} -> hardTypeError =<< notData
Sort{} -> hardTypeError =<< notData
Lam{} -> __IMPOSSIBLE__
Lit{} -> __IMPOSSIBLE__
Con{} -> __IMPOSSIBLE__
Level{} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
_ -> softTypeError =<< notData
where notData = liftTCM $ SplitError . NotADatatype <$> buildClosure a
getRecordConstructor
:: QName
-> Args
-> Type
-> TCM (ConHead, Type)
getRecordConstructor d pars a = do
con <- (theDef <$> getConstInfo d) >>= \case
Record{recConHead = con} -> return $ killRange con
_ -> typeError $ ShouldBeRecordType a
b <- (`piApply` pars) . defType <$> getConstInfo (conName con)
return (con, b)
disambiguateProjection
:: Hiding
-> AmbiguousQName
-> Arg Type
-> TCM (QName, Arg Type)
disambiguateProjection h ambD@(AmbQ ds) b = do
caseMaybeM (liftTCM $ isRecordType $ unArg b) notRecord $ \(r, vs, def) -> case def of
Record{ recFields = fs } -> do
reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "we are of record type r = " ++ prettyShow r
, text "applied to parameters vs = " <+> prettyTCM vs
, text $ "and have fields fs = " ++ prettyShow fs
]
disambiguations <- mapM (runExceptT . tryProj False fs r vs) ds
case partitionEithers $ toList disambiguations of
(_ , (d,a):_) -> do
liftTCM $ storeDisambiguatedName d
return (d,a)
(_ , [] ) -> do
disambiguations <- mapM (runExceptT . tryProj True fs r vs) ds
case partitionEithers $ toList disambiguations of
([] , [] ) -> __IMPOSSIBLE__
(err:_, [] ) -> throwError err
(errs , [(d,a)]) -> do
liftTCM $ storeDisambiguatedName d
return (d,a)
(errs , disambs@((d,a):_)) -> typeError . GenericDocError =<< vcat
[ text "Ambiguous projection " <> prettyTCM (qnameName d) <> text "."
, text "It could refer to any of"
, nest 2 $ vcat $ map showDisamb disambs
]
_ -> __IMPOSSIBLE__
where
showDisamb (d,_) =
let r = head $ filter (noRange /=) $ map nameBindingSite $ reverse $ mnameToList $ qnameModule d
in (pretty =<< dropTopLevelModule d) <+> text "(introduced at " <> prettyTCM r <> text ")"
notRecord = wrongProj $ headNe ds
wrongProj :: (MonadTCM m, MonadError TCErr m) => QName -> m a
wrongProj d = softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ text "Cannot eliminate type "
, prettyTCM (unArg b)
, text " with projection "
, if isAmbiguous ambD then
text . prettyShow =<< dropTopLevelModule d
else
prettyTCM d
]
wrongHiding :: (MonadTCM m, MonadError TCErr m) => QName -> m a
wrongHiding d = softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ text "Wrong hiding used for projection " , prettyTCM d ]
tryProj
:: Bool
-> [Arg QName]
-> QName
-> Args
-> QName
-> ExceptT TCErr TCM (QName, Arg Type)
tryProj constraintsOk fs r vs d0 = isProjection d0 >>= \case
Nothing -> wrongProj d0
Just proj -> do
let d = projOrig proj
qr <- maybe (wrongProj d) return $ projProper proj
when (null $ projLams proj) $ wrongProj d
reportSLn "tc.lhs.split" 90 "we are a projection pattern"
reportSDoc "tc.lhs.split" 20 $ sep
[ text $ "proj d0 = " ++ prettyShow d0
, text $ "original proj d = " ++ prettyShow d
]
argd <- maybe (wrongProj d) return $ List.find ((d ==) . unArg) fs
let ai = setRelevance (getRelevance argd) $ projArgInfo proj
unless (sameHiding h ai) $ wrongHiding d
suspendErrors $ applyUnless constraintsOk noConstraints $
checkParameters qr r vs
dType <- liftTCM $ defType <$> getConstInfo d
reportSDoc "tc.lhs.split" 20 $ sep
[ text "we are being projected by dType = " <+> prettyTCM dType
]
projType <- liftTCM $ dType `piApplyM` vs
return (d0 , Arg ai projType)
disambiguateConstructor
:: AmbiguousQName
-> QName
-> Args
-> TCM (ConHead, Type)
disambiguateConstructor ambC@(AmbQ cs) d pars = do
d <- canonicalName d
cons <- theDef <$> getConstInfo d >>= \case
def@Datatype{} -> return $ dataCons def
def@Record{} -> return $ [conName $ recConHead def]
_ -> __IMPOSSIBLE__
disambiguations <- mapM (runExceptT . tryCon False cons d pars) cs
case partitionEithers $ toList disambiguations of
(_ , (c0,c,a):_) -> do
when (isAmbiguous ambC) $ liftTCM $ storeDisambiguatedName c0
return (c,a)
(_ , [] ) -> do
disambiguations <- mapM (runExceptT . tryCon True cons d pars) cs
case partitionEithers $ toList disambiguations of
([] , [] ) -> __IMPOSSIBLE__
(err:_, [] ) -> throwError err
(errs , [(c0,c,a)]) -> do
when (isAmbiguous ambC) $ liftTCM $ storeDisambiguatedName c0
return (c,a)
(errs , disambs@((c0,c,a):_)) -> typeError . GenericDocError =<< vcat
[ text "Ambiguous constructor " <> prettyTCM (qnameName $ conName c) <> text "."
, text "It could refer to any of"
, nest 2 $ vcat $ map showDisamb disambs
]
where
showDisamb (c0,_,_) =
let r = head $ filter (noRange /=) $ map nameBindingSite $ reverse $ mnameToList $ qnameModule c0
in (pretty =<< dropTopLevelModule c0) <+> text "(introduced at " <> prettyTCM r <> text ")"
abstractConstructor c = softTypeError $
AbstractConstructorNotInScope c
wrongDatatype c d = softTypeError $
ConstructorPatternInWrongDatatype c d
tryCon
:: Bool
-> [QName]
-> QName
-> Args
-> QName
-> ExceptT TCErr TCM (QName, ConHead, Type)
tryCon constraintsOk cons d pars c = getConstInfo' c >>= \case
Left (SigUnknown err) -> __IMPOSSIBLE__
Left SigAbstract -> abstractConstructor c
Right def -> do
let con = conSrcCon $ theDef def
unless (conName con `elem` cons) $ wrongDatatype c d
suspendErrors $ applyUnless constraintsOk noConstraints $
checkConstructorParameters c d pars
cType <- (`piApply` pars) . defType <$> getConInfo con
return (c, con, cType)
checkConstructorParameters :: MonadTCM tcm => QName -> QName -> Args -> tcm ()
checkConstructorParameters c d pars = do
dc <- liftTCM $ getConstructorData c
checkParameters dc d pars
checkParameters
:: MonadTCM tcm
=> QName
-> QName
-> Args
-> tcm ()
checkParameters dc d pars = liftTCM $ do
a <- reduce (Def dc [])
case a of
Def d0 es -> do
let vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
reportSDoc "tc.lhs.split" 40 $
vcat [ nest 2 $ text "d =" <+> (text . prettyShow) d
, nest 2 $ text "d0 (should be == d) =" <+> (text . prettyShow) d0
, nest 2 $ text "dc =" <+> (text . prettyShow) dc
, nest 2 $ text "vs =" <+> prettyTCM vs
]
t <- typeOfConst d
compareArgs [] [] t (Def d []) vs (take (length vs) pars)
_ -> __IMPOSSIBLE__
checkSortOfSplitVar :: (MonadTCM tcm, MonadError TCErr tcm, LensSort a) => a -> tcm ()
checkSortOfSplitVar a = liftTCM (reduce $ getSort a) >>= \case
Type{} -> return ()
_ -> softTypeError =<< do
liftTCM $ GenericDocError <$> sep
[ text "Cannot split on datatype in sort" , prettyTCM (getSort a) ]