@@ -1772,17 +1772,16 @@ addImpl' inpat env infns imp_meths ist ptm
1772 (ai inpat qq env ds t)
1772 (ai inpat qq env ds t)
1773 (ai inpat qq env ds f)
1773 (ai inpat qq env ds f)
1775− -- If the name in a lambda is a constructor name, do this as a 'case'
1775+ -- If the name in a lambda is an unapplied data constructor name, do this
1776− -- instead (it is harmless to do so, especially since the lambda will
1776+ -- as a 'case' instead because we'll expect to match on it
1777− -- be lifted anyway!)
1778 ai inpat qq env ds (PLam fc n nfc ty sc)
1777 ai inpat qq env ds (PLam fc n nfc ty sc)
1779− = case lookupDef n (tt_ctxt ist) of
1778+ = if canBeDConName n (tt_ctxt ist)
1780− [] -> let ty' = ai inpat qq env ds ty
1781− sc' = ai inpat qq ((n, Just ty):env) ds sc in
1782− PLam fc n nfc ty' sc'
1783− _ -> ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1779+ then ai inpat qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
1784 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1780 (PCase fc (PRef fc [] (sMN 0 "lamp") )
1785 [(PRef fc [] n, sc)]))
1781 [(PRef fc [] n, sc)]))
1782+ else let ty' = ai inpat qq env ds ty
1783+ sc' = ai inpat qq ((n, Just ty):env) ds sc in
1784+ PLam fc n nfc ty' sc'
1786 ai inpat qq env ds (PLet fc n nfc ty val sc)
1785 ai inpat qq env ds (PLet fc n nfc ty val sc)
1787 = case lookupDef n (tt_ctxt ist) of
1786 = case lookupDef n (tt_ctxt ist) of
1788 [] -> let ty' = ai inpat qq env ds ty
1787 [] -> let ty' = ai inpat qq env ds ty