Better partial evaluation of polymorphic HOFs

Need to make sure types constructors are stripped on the LHS or they
won't get past the elaborator.

src/Idris/AbsSyntax.hs

@@ -1815,9 +1815,13 @@ stripLinear i tm = evalState (sl tm) [] where
 stripUnmatchable :: IState -> PTerm -> PTerm
 stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
     su :: PTerm -> PTerm
-    su (PRef fc f)
+    su tm@(PRef fc f)
        | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)
           = Placeholder
+       | (TType _ : _) <- lookupTy f (tt_ctxt i)
+          = PHidden tm
+       | (UType _ : _) <- lookupTy f (tt_ctxt i)
+          = PHidden tm
     su (PApp fc f@(PRef _ fn) args)
        -- here we use canBeDConName because the impossible pattern
        -- check will not necessarily fully resolve constructor names,

src/Idris/Elab/Clause.hs

@@ -373,7 +373,7 @@ elabPE info fc caller r =
                 logLvl 3 $ "PE definition " ++ show newnm ++ ":\n" ++
                              showSep "\n"
                                 (map (\ (lhs, rhs) ->
-                                  (show lhs ++ " = " ++
+                                  (showTmImpls lhs ++ " = " ++
                                    showTmImpls rhs)) (pe_clauses specdecl))
 
                 logLvl 2 $ show n ++ " transformation rule: " ++
@@ -381,7 +381,8 @@ elabPE info fc caller r =
 
                 elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy
                 let def = map (\(lhs, rhs) ->
-                                  PClause fc newnm lhs [] rhs []) 
+                                 let lhs' = mapPT hiddenToPH $ stripUnmatchable ist lhs in
+                                  PClause fc newnm lhs' [] rhs []) 
                               (pe_clauses specdecl)    
                 trans <- elabTransform info fc False rhs lhs
                 elabClauses info fc (PEGenerated:opts) newnm def
@@ -393,6 +394,9 @@ elabPE info fc caller r =
           (\e -> do logLvl 3 $ "Couldn't specialise: " ++ (pshow ist e)
                     return [])
 
+    hiddenToPH (PHidden _) = Placeholder
+    hiddenToPH x = x
+
     specName simpl (ImplicitS, tm)
         | (P Ref n _, _) <- unApply tm = Just (n, Just (if simpl then 1 else 0))
     specName simpl (ExplicitS, tm)

src/Idris/PartialEval.hs

@@ -197,6 +197,7 @@ mkNewPats ist d ns newname sname lhs rhs | all dynVar (map fst d)
         dynArgs (_ : ns) (V _     : as) = dynArgs ns as
         dynArgs (_ : ns) (P _ _ _ : as) = dynArgs ns as
         dynArgs _ _ = False -- and now we'll get stuck 
+
 mkNewPats ist d ns newname sname lhs rhs =
     PEDecl lhs rhs (map mkClause d) False
   where 
@@ -235,7 +236,7 @@ mkNewPats ist d ns newname sname lhs rhs =
     mkSubst :: (Term, Term) -> Maybe (Name, Term)
     mkSubst (P _ n _, t) = Just (n, t)
     mkSubst _ = Nothing
-
+        
 -- | Creates a new declaration for a specialised function application.
 -- Simple version at the moment: just create a version which is a direct
 -- application of the function to be specialised.

test/reg054/expected

@@ -3,7 +3,9 @@ When checking an application of constructor Main.MkInfer:
         Attempting concrete match on polymorphic argument: 0
 reg054.idr:34:7:When checking left hand side of weird:
 No explicit types on left hand side: Char
-reg054.idr:37:1-8:When checking left hand side of tctrick:
+reg054.idr:37:8:When checking left hand side of weird':
+No explicit types on left hand side: Nat
+reg054.idr:40:1-8:When checking left hand side of tctrick:
 When checking an application of Main.tctrick:
         Type mismatch between
                 Maybe a1 (Type of Just x)

test/reg054/reg054.idr

@@ -33,6 +33,9 @@ data Weird : Type -> Type where
 weird : Weird x -> x
 weird {x = Char} y = '5'
 
+weird' : Weird x -> x
+weird' {x = Prelude.Nat.Nat} y = Z
+
 tctrick : a -> Int
 tctrick (Just x) = x
 tctrick Nothing = 42