functions that should not expect types

Stream: lean4

[Jared green]

(v4.6.0-rc1)
why would these functions expect types?:

import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
open Classical
variable (α : Type)[h : DecidableEq α]
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred

namespace normalizable

def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)

--no, these functions absolutely should not be expecting types
def subnormalize (n : (normalizable α pred)) : List (List (List (normalizable α pred))) :=
  match n with
  | Or a b => [[a,n],[b,n],[Not a,Not b, Not n]] :: (List.append (subnormalize a) (subnormalize b))
  | And a b => [[a,b,n],[Not a,Not n],[Not b,Not n]] :: (List.append (subnormalize a) (subnormalize b))
  | Not i => [[n,Not i],[Not n, i]] :: (subnormalize i)
  | atom _ => [[[n],[Not n]]]

def normalize :  normalizable α pred -> List (List (List (normalizable α pred))) := fun o =>
  [[o]] :: (subnormalize o) --first error here

def nStrip (n : normalizable α pred) : Bool × normalizable α pred :=
  match n with
  | Not (Not i) => nStrip i
  | Not i => (false,i)
  |i => (true,i)

def normalizel (n : normalizable α pred) : List (List (List (Bool × normalizable α pred))) :=
  (normalize n).map (fun x => x.map (fun y => y.map (fun z => nStrip z)))

def wToProp (w : Bool × normalizable α pred) : Prop :=
  if w.fst then toProp w.snd else ¬(toProp w.snd)

def sToProp (s : List (Bool × normalizable α pred)) : Prop :=
  (s.map (fun x => wToProp x)).foldr ∧ true

def gToProp (g : List (List (Bool × normalizable α pred))) : Prop :=
  (g.map (fun x => sToProp x)).foldr ∨ false

def nToProp (n : List (List (List (Bool × normalizable α pred)))) : Prop :=
  (n.map (fun x => gToProp x)).foldr ∧ true

[Timo Carlin-Burns]

If I look at the output of #check subnormalize, it's first explicit parameter is (α : Type)

#check subnormalize -- normalizable.subnormalize (α : Type) {pred : α → Prop} (n : normalizable α pred) : List (List (List (normalizable α pred)))

This comes from variable (α : Type) above

[Jared green]

what can be done about it?

[Timo Carlin-Burns]

If you want to leave α implicit and have it be inferred, you can declare the parameter with curly braces instead of parentheses:

import Init.Data.List
import Std.Data.List
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Defs
open Classical
variable {α : Type}[h : DecidableEq α] -- < changed
inductive normalizable α (pred : α -> Prop)
  where
  | atom : α -> (normalizable α pred)
  | And : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Or : (normalizable α pred) -> (normalizable α pred) -> normalizable α pred
  | Not : normalizable α pred -> normalizable α pred

namespace normalizable

def toProp (n : normalizable α pred) : Prop :=
  match n with
  | atom a => pred a
  | And a b =>  toProp a ∧ toProp b
  | Or a b => (toProp a) ∨ toProp b
  | Not i => ¬(toProp i)


def subnormalize (n : (normalizable α pred)) : List (List (List (normalizable α pred))) :=
  match n with
  | Or a b => [[a,n],[b,n],[Not a,Not b, Not n]] :: (List.append (subnormalize a) (subnormalize b))
  | And a b => [[a,b,n],[Not a,Not n],[Not b,Not n]] :: (List.append (subnormalize a) (subnormalize b))
  | Not i => [[n,Not i],[Not n, i]] :: (subnormalize i)
  | atom _ => [[[n],[Not n]]]

def normalize :  normalizable α pred -> List (List (List (normalizable α pred))) := fun o =>
  [[o]] :: (subnormalize o) --no error!