@@ -395,6 +395,9 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
395395 ctxt <- getContext
396396 let cty' = normalise ctxt [] cty
397397
398+ -- Check that the constructor type is, in fact, a part of the family being defined
399+ tyIs n cty'
400+
398401 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
399402 logLvl 5 $ "Inaccessible args: " ++ show inacc
400403 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
@@ -407,11 +410,11 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
407410 addIBC (IBCOpt n)
408411 return (n, cty')
409412 where
410− tyIs (Bind n b sc) = tyIs sc
411− tyIs t | (P _ n' _, _) <- unApply t
412− = if n' /= tn then tclift $ tfail (At fc (Msg (show n' ++ " is not " ++ show tn)))
413+ tyIs con (Bind n b sc) = tyIs con sc
414+ tyIs con t | (P _ n' _, _) <- unApply t
415+ = if n' /= tn then tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show n' ++ " is not " ++ show tn))))
413416 else return ()
414− tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))
417+ tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))
415418
416419 mkLazy (PPi pl n ty sc)
417420 = let ty' = if getTyName ty