@@ -1847,6 +1847,8 @@ addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm
18471847addImpl' inpat env infns imp_meths ist ptm
18481848 = ai inpat False (zip env (repeat Nothing)) [] (mkUniqueNames env [] ptm)
18491849 where
1850+ allowcap = AllowCapitalizedPatternVariables `elem` opt_cmdline (idris_options ist)
1851+
18501852 topname = case ptm of
18511853 PRef _ _ n -> n
18521854 PApp _ (PRef _ _ n) _ -> n
@@ -1855,9 +1857,9 @@ addImpl' inpat env infns imp_meths ist ptm
18551857 ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm
18561858 ai inpat qq env ds (PRef fc fcs f)
18571859 | f `elem` infns = PInferRef fc fcs f
1858− | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []
1860+ | not (f `elem` map fst env) = handleErr $ aiFn topname allowcap inpat inpat qq imp_meths ist fc f fc ds []
18591861 ai inpat qq env ds (PHidden (PRef fc hl f))
1860− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])
1862+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname allowcap inpat False qq imp_meths ist fc f fc ds [])
18611863 ai inpat qq env ds (PRewrite fc by l r g)
18621864 = let l' = ai inpat qq env ds l
18631865 r' = ai inpat qq env ds r
@@ -1887,7 +1889,7 @@ addImpl' inpat env infns imp_meths ist ptm
18871889 | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as)
18881890 | not (f `elem` map fst env)
18891891 = let as' = map (fmap (ai inpat qq env ds)) as in
1890− handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as'
1892+ handleErr $ aiFn topname allowcap inpat False qq imp_meths ist fc f ffc ds as'
18911893 | Just (Just ty) <- lookup f env =
18921894 let as' = map (fmap (ai inpat qq env ds)) as
18931895 arity = getPArity ty in
@@ -1972,28 +1974,31 @@ addImpl' inpat env infns imp_meths ist ptm
19721974-- if in a pattern, and there are no arguments, and there's no possible
19731975-- names with zero explicit arguments, don't add implicits.
19741976
1975−aiFn :: Name -> Bool -> Bool -> Bool
1977+aiFn :: Name -> Bool -- ^ Allow capitalization of pattern variables
1978+ -> Bool -> Bool -> Bool
19761979 -> [Name]
19771980 -> IState -> FC
19781981 -> Name -- ^ function being applied
19791982 -> FC -> [[T.Text]]
19801983 -> [PArg] -- ^ initial arguments (if in a pattern)
19811984 -> Either Err PTerm
1982−aiFn topname inpat True qq imp_meths ist fc f ffc ds []
1985+aiFn topname allowcap inpat True qq imp_meths ist fc f ffc ds []
19831986 | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f
19841987 | otherwise
19851988 = case lookupDef f (tt_ctxt ist) of
1986− [] -> case f of
1987− MN _ _ -> Right $ PPatvar ffc f
1988− UN xs | isDigit (T.head xs) -- for partial evaluation vars
1989− -> Right $ PPatvar ffc f
1990− _ -> Left $ Msg $ show f ++ " is not a valid name for a pattern variable"
1989+ [] -> if allowcap
1990+ then Right $ PPatvar ffc f
1991+ else case f of
1992+ MN _ _ -> Right $ PPatvar ffc f
1993+ UN xs | isDigit (T.head xs) -- for partial evaluation vars
1994+ -> Right $ PPatvar ffc f
1995+ _ -> Left $ Msg $ show f ++ " is not a valid name for a pattern variable"
19911996 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in
19921997 -- trace (show f ++ " " ++ show (fc, any (all imp) ialts, ialts, any constructor alts)) $
19931998 if (not (vname f) || tcname f
19941999 || any (conCaf (tt_ctxt ist)) ialts)
19952000-- any constructor alts || any allImp ialts))
1996− then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
2001+ then aiFn topname allowcap inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor
19972002 else Right $ PPatvar ffc f
19982003 where imp (PExp _ _ _ _) = False
19992004 imp _ = True
@@ -2008,9 +2013,9 @@ aiFn topname inpat True qq imp_meths ist fc f ffc ds []
20082013 vname (UN n) = True -- non qualified
20092014 vname _ = False
20102015
2011−aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
2016+aiFn topname allowcap inpat expat qq imp_meths ist fc f ffc ds as
20122017 | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as
2013−aiFn topname inpat expat qq imp_meths ist fc f ffc ds as
2018+aiFn topname allowcap inpat expat qq imp_meths ist fc f ffc ds as
20142019 -- This is where namespaces get resolved by adding PAlternative
20152020 = do let ns = lookupCtxtName f (idris_implicits ist)
20162021 let nh = filter (\(n, _) -> notHidden n) ns