Fix invalid implementation message
It's not so much about injectivity, as that we need to be able to
retrieve the arguments, and we can only do that with type or data
constructors
commit9e13367bc9d38662c3e3c6781cbb886f2629c1b6
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateWed 15 Jun 2016, 20:43 (10 years ago)
parent55230b7
src/Idris/Delaborate.hs+1−1
@@ -364,7 +364,7 @@ pprintErr' i (CantResolve _ c e)
364364pprintErr' i (InvalidTCArg n t)
365365 = annTm t (pprintTerm i (delabSugared i t)) <+> text " cannot be a parameter of "
366366 <> annName n <$>
367− text "(Implementation arguments must be injective)"
367+ text "(Implementation arguments must be type or data constructors)"
368368pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
369369 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as)))
370370pprintErr' i (NoValidAlts as) = text "Can't disambiguate since no name has a suitable type:" <+>