Optional params break sorry

[digama0]

The sorry term fails when the goal is a forall type with trailing opt params, likely due to inconsistent handling of whether to introduce the parameter. The sorry tactic is unaffected.

def foo : (_ : Nat := 0) → Nat := sorry
                               -- ^^^^^
-- type mismatch
--   sorryAx (optParam Nat 0 → Nat) false
-- has type
--   Nat : Type
-- but is expected to have type
--   optParam Nat 0 → Nat : Type

def foo' : (_ : Nat := 0) → Nat := by sorry -- ok