module Agda.TypeChecking.Rules.LHS where
import Data.Maybe
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Data.Traversable
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses
import Agda.Syntax.Internal as I hiding (Substitution)
import Agda.Syntax.Internal.Pattern
import Agda.Syntax.Abstract (IsProjP(..))
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Views (asView)
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Position
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Empty
import Agda.TypeChecking.Patterns.Abstract
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Records
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute hiding (Substitution)
import qualified Agda.TypeChecking.Substitute as S (Substitution)
import Agda.TypeChecking.Telescope
import 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.Split
import Agda.TypeChecking.Rules.LHS.Implicit
import Agda.TypeChecking.Rules.LHS.Instantiate
import Agda.TypeChecking.Rules.Data
import Agda.Utils.Functor (($>))
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
#include "undefined.h"
import Agda.Utils.Impossible
flexiblePatterns :: [A.NamedArg A.Pattern] -> TCM FlexibleVars
flexiblePatterns nps = map setFlex <$> filterM (flexible . namedArg . snd) (zip [0..] $ reverse nps)
where
setFlex (i, Arg ai p) = FlexibleVar (getHiding ai) (classify $ namedThing p) i
classify A.DotP{} = DotFlex
classify A.ImplicitP{} = ImplicitFlex
classify A.ConP{} = RecordFlex
classify _ = __IMPOSSIBLE__
flexible (A.DotP _ _) = return True
flexible (A.ImplicitP _) = return True
flexible (A.ConP _ (A.AmbQ [c]) qs) =
ifM (isJust <$> isRecordConstructor c)
(andM $ map (flexible . namedArg) qs)
(return False)
flexible _ = return False
dotPatternInsts :: [A.NamedArg A.Pattern] -> Substitution -> [I.Dom Type] -> TCM [DotPatternInst]
dotPatternInsts ps s as = dpi (map namedArg ps) (reverse s) as
where
dpi (_ : _) [] _ = __IMPOSSIBLE__
dpi (_ : _) (Just _ : _) [] = __IMPOSSIBLE__
dpi [] _ _ = return []
dpi (_ : ps) (Nothing : s) as = dpi ps s as
dpi (p : ps) (Just u : s) (a : as) =
case p of
A.DotP _ e -> (DPI e u a :) <$> dpi ps s as
A.ImplicitP _ -> dpi ps s as
A.ConP _ (A.AmbQ [c]) qs -> do
Def r es <- ignoreSharing <$> reduce (unEl $ unDom a)
let Just vs = allApplyElims es
(ftel, us) <- etaExpandRecord r vs u
qs <- insertImplicitPatterns ExpandLast qs ftel
let instTel EmptyTel _ = []
instTel (ExtendTel arg tel) (u : us) = arg : instTel (absApp tel u) us
instTel ExtendTel{} [] = __IMPOSSIBLE__
bs0 = instTel ftel (map unArg us)
bs = map (mapRelevance (composeRelevance (getRelevance a))) bs0
dpi (map namedArg qs ++ ps) (map (Just . unArg) us ++ s) (bs ++ as)
_ -> __IMPOSSIBLE__
instantiatePattern :: Substitution -> Permutation -> [I.NamedArg Pattern] -> [I.NamedArg Pattern]
instantiatePattern sub perm ps
| length sub /= length hps = error $ unlines [ "instantiatePattern:"
, " sub = " ++ show sub
, " perm = " ++ show perm
, " ps = " ++ show ps
]
| otherwise = foldr merge ps $ zipWith inst (reverse sub) hps
where
hps = permute perm $ allHoles ps
inst Nothing hps = Nothing
inst (Just t) hps = Just $ plugHole (DotP t) hps
merge Nothing ps = ps
merge (Just qs) ps = zipWith mergeA qs ps
where
mergeA a1 a2 = fmap (mergeP (namedArg a1) (namedArg a2) <$) a1
mergeP (DotP s) (DotP t)
| s == t = DotP s
| otherwise = __IMPOSSIBLE__
mergeP (DotP t) (VarP _) = DotP t
mergeP (VarP _) (DotP t) = DotP t
mergeP (DotP _) _ = __IMPOSSIBLE__
mergeP _ (DotP _) = __IMPOSSIBLE__
mergeP (ConP c1 mt1 ps) (ConP c2 mt2 qs)
| c1 == c2 = ConP (c1 `withRangeOf` c2) (mplus mt1 mt2) $ zipWith mergeA ps qs
| otherwise = __IMPOSSIBLE__
mergeP (LitP l1) (LitP l2)
| l1 == l2 = LitP (l1 `withRangeOf` l2)
| otherwise = __IMPOSSIBLE__
mergeP (VarP x) (VarP y)
| x == y = VarP x
| otherwise = __IMPOSSIBLE__
mergeP (ConP _ _ _) (VarP _) = __IMPOSSIBLE__
mergeP (ConP _ _ _) (LitP _) = __IMPOSSIBLE__
mergeP (VarP _) (ConP _ _ _) = __IMPOSSIBLE__
mergeP (VarP _) (LitP _) = __IMPOSSIBLE__
mergeP (LitP _) (ConP _ _ _) = __IMPOSSIBLE__
mergeP (LitP _) (VarP _) = __IMPOSSIBLE__
mergeP (ProjP x) (ProjP y)
| x == y = ProjP x
| otherwise = __IMPOSSIBLE__
mergeP ProjP{} _ = __IMPOSSIBLE__
mergeP _ ProjP{} = __IMPOSSIBLE__
isSolvedProblem :: Problem -> Bool
isSolvedProblem problem = null (restPats $ problemRest problem) &&
all (isSolved . snd . asView . namedArg) (problemInPat problem)
where
isSolved (A.DefP _ _ []) = False
isSolved (A.VarP _) = True
isSolved (A.WildP _) = True
isSolved (A.ImplicitP _) = True
isSolved (A.AbsurdP _) = True
isSolved _ = False
noShadowingOfConstructors
:: (Maybe r -> Call)
-> Problem -> TCM ()
noShadowingOfConstructors mkCall problem =
traceCall mkCall $ do
let pat = map (snd . asView . namedArg) $
problemInPat problem
tel = map (unEl . snd . unDom) $ telToList $ problemTel problem
zipWithM noShadowing pat tel
return ()
where
noShadowing (A.WildP {}) t = return ()
noShadowing (A.AbsurdP {}) t = return ()
noShadowing (A.ImplicitP {}) t = return ()
noShadowing (A.ConP {}) t = return ()
noShadowing (A.DefP {}) t = return ()
noShadowing (A.AsP {}) t = __IMPOSSIBLE__
noShadowing (A.DotP {}) t = __IMPOSSIBLE__
noShadowing (A.LitP {}) t = __IMPOSSIBLE__
noShadowing (A.PatternSynP {}) t = __IMPOSSIBLE__
noShadowing (A.VarP x) t = do
reportSDoc "tc.lhs.shadow" 30 $ vcat
[ text $ "checking whether pattern variable " ++ show x ++ " shadows a constructor"
, nest 2 $ text "type of variable =" <+> prettyTCM t
]
reportSLn "tc.lhs.shadow" 70 $ " t = " ++ show t
t <- reduce t
case t 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 (getRange x) $
typeError $ PatternShadowsConstructor x c
Axiom {} -> return ()
Function {} -> return ()
Record {} -> return ()
Constructor {} -> __IMPOSSIBLE__
Primitive {} -> __IMPOSSIBLE__
Var {} -> return ()
Pi {} -> return ()
Sort {} -> return ()
Shared p -> noShadowing (A.VarP x) $ derefPtr p
MetaV {} -> return ()
Lam {} -> __IMPOSSIBLE__
Lit {} -> __IMPOSSIBLE__
Level {} -> __IMPOSSIBLE__
Con {} -> __IMPOSSIBLE__
DontCare{} -> __IMPOSSIBLE__
ExtLam{} -> __IMPOSSIBLE__
checkDotPattern :: DotPatternInst -> TCM ()
checkDotPattern (DPI 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 (argInfoRelevance info) $ do
u <- checkExpr e a
noConstraints $ equalTerm a u v
bindLHSVars :: [A.NamedArg A.Pattern] -> Telescope -> TCM a -> TCM a
bindLHSVars [] tel@ExtendTel{} _ = do
reportSDoc "impossible" 10 $
text "bindLHSVars: no patterns left, but tel =" <+> prettyTCM tel
__IMPOSSIBLE__
bindLHSVars (_ : _) EmptyTel _ = __IMPOSSIBLE__
bindLHSVars [] EmptyTel ret = ret
bindLHSVars (p : ps) (ExtendTel a tel) ret =
case namedArg p of
A.VarP x -> addContext (x, a) $ bindLHSVars ps (absBody tel) ret
A.WildP _ -> bindDummy (absName tel)
A.ImplicitP _ -> bindDummy (absName tel)
A.AbsurdP pi -> do
isEmptyType (getRange pi) $ unDom a
bindDummy (absName tel)
A.ConP _ (A.AmbQ [c]) qs -> do
Def r es <- reduce (unEl $ unDom a)
let Just vs = allApplyElims es
ftel <- (`apply` vs) <$> getRecordFieldTypes r
con <- getConHead c
let n = size ftel
eta = Con con [ var i <$ (namedThing <$> setArgColors [] q) | (q, i) <- zip qs [n 1, n 2..0] ]
bindLHSVars (qs ++ ps) (ftel `abstract` absApp (raise (size ftel) tel) eta) ret
A.ConP{} -> __IMPOSSIBLE__
A.DefP{} -> __IMPOSSIBLE__
A.AsP{} -> __IMPOSSIBLE__
A.DotP{} -> __IMPOSSIBLE__
A.LitP{} -> __IMPOSSIBLE__
A.PatternSynP{} -> __IMPOSSIBLE__
where
bindDummy s = do
x <- if isUnderscore s then freshNoName_ else freshName_ ("." ++ argNameToString s)
addContext (x, a) $ bindLHSVars ps (absBody tel) ret
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
data LHSResult = LHSResult
{ lhsPatternTele :: Maybe Telescope
, lhsVarTele :: Telescope
, lhsSubstitution :: S.Substitution
, lhsVarNames :: [String]
, lhsPatterns :: [I.NamedArg Pattern]
, lhsBodyType :: I.Arg Type
, lhsPermutation :: Permutation
}
checkLeftHandSide
:: (Maybe r -> Call)
-> Maybe QName
-> [A.NamedArg A.Pattern]
-> Type
-> (LHSResult -> TCM a)
-> TCM a
checkLeftHandSide c f ps a ret = do
problem0 <- problemFromPats ps a
let mgamma = if noProblemRest problem0 then Just $ problemTel problem0 else Nothing
LHSState problem@(Problem ps (perm, qs) delta rest) sigma dpi asb
<- checkLHS f $ LHSState problem0 idS [] []
unless (null $ restPats rest) $ typeError $ TooManyArgumentsInLHS a
noShadowingOfConstructors c problem
noPatternMatchingOnCodata qs
reportSDoc "tc.lhs.top" 10 $
vcat [ text "checked lhs:"
, nest 2 $ vcat
[ text "ps = " <+> fsep (map prettyA ps)
, text "perm = " <+> text (show perm)
, text "delta = " <+> prettyTCM delta
, text "dpi = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi)
, text "asb = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb)
, text "qs = " <+> text (show qs)
]
]
let b' = restType rest
bindLHSVars (filter (isNothing . isProjP) ps) delta $ bindAsPatterns asb $ do
reportSDoc "tc.lhs.top" 10 $ text "bound pattern variables"
reportSDoc "tc.lhs.top" 10 $ nest 2 $ text "type = " <+> prettyTCM b'
mapM_ checkDotPattern dpi
let rho = renamingR perm
Perm n _ = perm
xs = [ stringToArgName $ "h" ++ show n | n <- [0..n 1] ]
applyRelevanceToContext (getRelevance b') $ do
ret $ LHSResult mgamma delta rho xs qs b' perm
checkLHS
:: Maybe QName
-> LHSState
-> TCM LHSState
checkLHS f st@(LHSState problem sigma dpi asb) = do
problem <- insertImplicitProblem problem
if isSolvedProblem problem then return $ st { lhsProblem = problem } else do
unlessM (optPatternMatching <$> gets getPragmaOptions) $
typeError $ GenericError $ "Pattern matching is disabled"
sp <- splitProblem f problem
reportSDoc "tc.lhs.split" 20 $ text "splitting completed"
case sp of
Left NothingToSplit -> do
reportSLn "tc.lhs.split" 50 $ "checkLHS: nothing to split in problem " ++ show problem
nothingToSplitError problem
Left (SplitPanic err) -> do
reportSLn "impossible" 10 $ "checkLHS: panic: " ++ err
__IMPOSSIBLE__
Right (SplitRest projPat projType) -> do
let Problem ps1 (iperm, ip) delta (ProblemRest (p:ps2) b) = problem
ps' = ps1
rest = ProblemRest ps2 (projPat $> projType)
ip' = ip ++ [fmap (Named Nothing . ProjP) projPat]
problem' = Problem ps' (iperm, ip') delta rest
st' <- updateProblemRest (LHSState problem' sigma dpi asb)
applyRelevanceToContext (getRelevance projPat) $ do
checkLHS f st'
Right (Split p0 xs (Arg _ (LitFocus lit iph hix a)) p1) -> do
let ip = plugHole (LitP lit) iph
iperm = expandP hix 0 $ fst (problemOutPat problem)
let delta1 = problemTel p0
delta2 = absApp (fmap problemTel p1) (Lit lit)
rho = liftS (size delta2) $ singletonS (Lit lit)
sigma' = applySubst rho sigma
dpi' = applySubst rho dpi
asb0 = applySubst rho asb
ip' = applySubst rho ip
rest' = applySubst rho (problemRest problem)
let ps' = problemInPat p0 ++ problemInPat (absBody p1)
delta' = abstract delta1 delta2
problem' = Problem ps' (iperm, ip') delta' rest'
asb' = raise (size delta2) (map (\x -> AsB x (Lit lit) a) xs) ++ asb0
st' <- updateProblemRest (LHSState problem' sigma' dpi' asb')
checkLHS f st'
Right (Split p0 xs (Arg info
( Focus { focusCon = c
, focusImplicit = impl
, focusConArgs = qs
, focusRange = r
, focusOutPat = iph
, focusHoleIx = hix
, focusDatatype = d
, focusParams = vs
, focusIndices = ws
, focusType = a
}
)) p1
) -> traceCall (CheckPattern (A.ConP (ConPatInfo impl $ PatRange r) (A.AmbQ [c]) qs)
(problemTel p0)
(El Prop $ Def d $ map Apply $ vs ++ ws)) $ do
let delta1 = problemTel p0
let typeOfSplitVar = Arg info a
reportSDoc "tc.lhs.split" 10 $ sep
[ text "checking lhs"
, nest 2 $ text "tel =" <+> prettyTCM (problemTel problem)
, nest 2 $ text "rel =" <+> (text $ show $ argInfoRelevance info)
]
reportSDoc "tc.lhs.split" 15 $ sep
[ text "split problem"
, nest 2 $ vcat
[ text "delta1 = " <+> prettyTCM delta1
, text "typeOfSplitVar =" <+> prettyTCM typeOfSplitVar
, text "focusOutPat =" <+> (text . show) iph
, text "delta2 = " <+> prettyTCM (problemTel $ absBody p1)
]
]
c <- (`withRangeOf` c) <$> getConForm c
ca <- defType <$> getConInfo c
reportSDoc "tc.lhs.split" 20 $ nest 2 $ vcat
[ text "ca =" <+> prettyTCM ca
, text "vs =" <+> prettyList (map prettyTCM vs)
]
let a = ca `piApply` vs
(gamma', ca, d', us) <- do
TelV gamma' ca@(El _ def) <- telView a
let Def d' es = ignoreSharing def
Just us = allApplyElims es
return (gamma', ca, d', us)
unless (d == d') $ typeError $ ShouldBeApplicationOf ca d'
gamma' <- return $ fmap (applyRelevance $ argInfoRelevance info) gamma'
qs' <- insertImplicitPatterns ExpandLast qs gamma'
unless (size qs' == size gamma') $
typeError $ WrongNumberOfConstructorArguments (conName c) (size gamma') (size qs')
let gamma = useNamesFromPattern qs' gamma'
da <- (`piApply` vs) . defType <$> getConstInfo d
flex <- flexiblePatterns (problemInPat p0 ++ qs')
let us' = drop (size vs) us
reportSDoc "tc.lhs.top" 15 $ addCtxTel delta1 $
sep [ text "preparing to unify"
, nest 2 $ vcat
[ text "c =" <+> prettyTCM c <+> text ":" <+> prettyTCM a
, text "d =" <+> prettyTCM d <+> text ":" <+> prettyTCM da
, text "gamma =" <+> prettyTCM gamma
, text "gamma' =" <+> prettyTCM gamma'
, text "vs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs)
, text "us' =" <+> brackets (fsep $ punctuate comma $ map prettyTCM us')
, text "ws =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws)
]
]
sub0 <- addCtxTel (delta1 `abstract` gamma) $
unifyIndices_ flex (raise (size gamma) da) us' (raise (size gamma) ws)
let ys = teleArgs gamma
delta2 = absApp (raise (size gamma) $ fmap problemTel p1) (Con c ys)
rho0 = liftS (size delta2) $ Con c ys :# raiseS (size gamma)
sigma0 = applySubst rho0 sigma
dpi0 = applySubst rho0 dpi
asb0 = applySubst rho0 asb
rest0 = applySubst rho0 (problemRest problem)
reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma) $ nest 2 $ vcat
[ text "delta2 =" <+> prettyTCM delta2
, text "sub0 =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub0)
]
reportSDoc "tc.lhs.top" 15 $ addCtxTel (delta1 `abstract` gamma `abstract` delta2) $
nest 2 $ vcat
[ text "dpi0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi0)
, text "asb0 = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb0)
]
storedPatternType <- ifM (isJust <$> isRecord d)
(return $ Just (impl, raise (1 + size delta2) typeOfSplitVar))
(return $ Nothing)
let ysp = map (argFromDom . fmap (namedVarP . fst)) $ telToList gamma
ip = plugHole (ConP c storedPatternType ysp) iph
ip0 = applySubst rho0 ip
let pad n xs x = xs ++ replicate (max 0 $ n size xs) x
newTel = problemTel p0 `abstract` (gamma `abstract` delta2)
sub = replicate (size delta2) Nothing ++
pad (size delta1 + size gamma) (raise (size delta2) sub0) Nothing
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "newTel =" <+> prettyTCM newTel
, addCtxTel newTel $ text "sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub)
, text "ip =" <+> text (show ip)
, text "ip0 =" <+> text (show ip0)
]
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "rho0 =" <+> text (show rho0)
]
(delta', perm, rho, instTypes) <- instantiateTel sub newTel
reportSDoc "tc.lhs.inst" 12 $
vcat [ sep [ text "instantiateTel"
, nest 4 $ brackets $ fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) sub
, nest 4 $ prettyTCM newTel
]
, nest 2 $ text "delta' =" <+> prettyTCM delta'
, nest 2 $ text "perm =" <+> text (show perm)
, nest 2 $ text "itypes =" <+> fsep (punctuate comma $ map prettyTCM instTypes)
]
let ps0' = problemInPat p0 ++ qs' ++ problemInPat (absBody p1)
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "subst rho sub =" <+> brackets (fsep $ punctuate comma $ map (maybe (text "_") prettyTCM) (applySubst rho sub))
, text "ps0' =" <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
]
newDpi <- dotPatternInsts ps0' (applySubst rho sub) instTypes
let dpi' = applySubst rho dpi0 ++ newDpi
asb' = applySubst rho $ asb0 ++ raise (size delta2) (map (\x -> AsB x (Con c ys) ca) xs)
reportSDoc "tc.lhs.top" 15 $ nest 2 $ vcat
[ text "dpi' = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi')
, text "asb' = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb')
]
let sigma' = applySubst rho sigma0
rest' = applySubst rho rest0
reportSDoc "tc.lhs.inst" 15 $
nest 2 $ text "ps0 = " <+> brackets (fsep $ punctuate comma $ map prettyA ps0')
let ps' = permute perm ps0'
let perm' = expandP hix (size gamma) $ fst (problemOutPat problem)
iperm' = perm `composeP` perm'
let ip' = instantiatePattern sub perm' ip0
newip = applySubst rho ip'
let problem' = Problem ps' (iperm', newip) delta' rest'
reportSDoc "tc.lhs.top" 12 $ sep
[ text "new problem"
, nest 2 $ vcat
[ text "ps' = " <+> fsep (map prettyA ps')
, text "delta' = " <+> prettyTCM delta'
]
]
reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
[ text "perm' =" <+> text (show perm')
, text "iperm' =" <+> text (show iperm')
]
reportSDoc "tc.lhs.top" 14 $ nest 2 $ vcat
[ text "ip' =" <+> text (show ip')
, text "newip =" <+> text (show newip)
]
st'@(LHSState problem'@(Problem ps' (iperm', ip') delta' rest')
sigma' dpi' asb')
<- updateProblemRest $ LHSState problem' sigma' dpi' asb'
reportSDoc "tc.lhs.top" 12 $ sep
[ text "new problem from rest"
, nest 2 $ vcat
[ text "ps' = " <+> fsep (map prettyA ps')
, text "delta' = " <+> prettyTCM delta'
, text "ip' =" <+> text (show ip')
, text "iperm' =" <+> text (show iperm')
]
]
checkLHS f st'
noPatternMatchingOnCodata :: [I.NamedArg Pattern] -> TCM ()
noPatternMatchingOnCodata = mapM_ (check . namedArg)
where
check (VarP {}) = return ()
check (DotP {}) = return ()
check (ProjP{}) = return ()
check (LitP {}) = return ()
check (ConP con _ ps) = do
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"