Fix long standing problem with kind of as binder (type recursion).

src/compiler/flx_bind/flx_bind_type.ml

@@ -312,13 +312,14 @@ print_endline ("FUDGE: Binding `TYP_var " ^ si i ^ ", HACKING KIND TO TYPE");
       btyp_type_var (i, Flx_kind.KIND_var "AnyKind")
     end
 
-  | `TYP_as (t,s) ->
+  | `TYP_as (t,s,k) ->
 (*
 print_endline ("\n\n+++++++++\nTrying to bind recursive type " ^ string_of_typecode t ^ " AS " ^ s);
 *)
+    let k = Flx_btype.bmt "Flx_bind_type:TYP_as" k in
     let t = bind_type'
       env
-      { rs with as_fixlist = (s,rs.depth)::rs.as_fixlist }
+      { rs with as_fixlist = (s,(rs.depth,k))::rs.as_fixlist }
       sr
       t
       params
@@ -491,9 +492,8 @@ print_endline ("  ***** Bound `TYP_apply: " ^ Flx_btype.st x );
   | `TYP_type_tuple ts -> btyp_type_tuple (List.map bt ts)
 
   | `TYP_name (sr,s,[]) when List.mem_assoc s rs.as_fixlist ->
-(* HACK metatype guess *)
-print_endline ("Flx_bind_type: as_fixlistL TYP_name metatype hack!");
-    btyp_fix ((List.assoc s rs.as_fixlist) - rs.depth) (Flx_kind.KIND_type)
+    let level, kind = List.assoc s rs.as_fixlist in
+    btyp_fix (level - rs.depth) kind 
 
   | `TYP_name (sr,s,[]) when List.mem_assoc s params ->
     let t = List.assoc s params in

src/compiler/flx_bind/flx_tpat.ml

@@ -84,7 +84,7 @@ let type_of_tpattern counter p =
 
        1 + int * list as list => list
     *)
-    | `TYP_as (t,n) ->
+    | `TYP_as (t,n,k) ->
       let t = tp t in
       let j = fresh_bid counter in
       as_vars := (j,n) :: !as_vars;

src/compiler/flx_bind/flx_typecode_of_btype.ml

@@ -59,7 +59,7 @@ let typecode_of_btype ?sym_table:(sym_table=None) bsym_table counter sr t0 =
     in
     if isrecursive then 
        let label = match mutrail with (_,label)::_ -> label | _ -> assert false in
-       `TYP_as (r,label)
+       `TYP_as (r,label,KND_type)
     else r
   in
   let r = tc 0 [] t0 in

src/compiler/flx_core/flx_ast.ml

@@ -127,7 +127,7 @@ and typecode_t = [
   | `TYP_borrowed of typecode_t                     (** uniq type *)
   | `TYP_array of typecode_t * typecode_t       (** array type base ^ index *)
   | `TYP_compactarray of typecode_t * typecode_t       (** array type base ^ index *)
-  | `TYP_as of typecode_t * Flx_id.t            (** fixpoint *)
+  | `TYP_as of typecode_t * Flx_id.t * kindcode_t (** fixpoint *)
   | `TYP_typeof of expr_t                       (** typeof *)
   | `TYP_var of index_t                         (** unknown type *)
   | `TYP_none                                   (** unspecified *)

src/compiler/flx_core/flx_btype.ml

@@ -1182,7 +1182,9 @@ and widen_fixgap level t =
     let fx t = adj (depth + 1) t in
     match map ~f_btype:fx t with
     | BTYP_fix (i, mt) when i + depth < 0 -> 
+(*
       print_endline ("Widening fixgap by " ^ string_of_int level);
+*)
       btyp_fix (i-level) mt
     | x -> x
   in adj 0 t

src/compiler/flx_core/flx_maps.ml

@@ -61,7 +61,7 @@ let map_type f (t:typecode_t):typecode_t = match t with
   | `TYP_borrowed t -> `TYP_borrowed (f t)
   | `TYP_array (t1, t2) -> `TYP_array (f t1, f t2)
   | `TYP_compactarray (t1, t2) -> `TYP_compactarray (f t1, f t2)
-  | `TYP_as (t,s) -> `TYP_as (f t,s)
+  | `TYP_as (t,s,k) -> `TYP_as (f t,s,k)
 
   (* type sets *)
   | `TYP_typeset ts -> `TYP_typeset (List.map f ts)

src/compiler/flx_core/flx_print.ml

@@ -579,7 +579,7 @@ and st prec tc : string =
     | `TYP_borrowed t -> 1,"borrowed[" ^ st 0 t ^ "]"
 
     | `TYP_typeof e -> 0,"typeof(" ^ string_of_expr e ^ ")"
-    | `TYP_as (t,s) -> 0, "([" ^ st 0 t ^ "] as " ^ string_of_id s ^ ")"
+    | `TYP_as (t,s,k) -> 0, "([" ^ st 0 t ^ "] as " ^ string_of_id s ^ ":" ^str_of_kindcode k^")"
 
     | `TYP_dual t -> 2,"~"^ st 2 t
 

src/compiler/flx_core/flx_type_fun.ml

@@ -100,7 +100,9 @@ Unfortunately this means the trail comparison must use alpha equivalance, not eq
 NOTE: alpha equiv is easy, we alph convert both terms using the SAME initial counter then 
 do normal comparison .. but I think maybe the type equality routine should do this.
 *)
+(*
 if not (Flx_btype.complete_type arg) then print_endline ("Type lambda argument is not complete! \n" ^ Flx_btype.st arg);
+*)
       let f = Flx_alpha.alpha_convert counter f in
       (* I think this is wrong but it is essential in some case if the argument
          must be a type tuple, and is actually an application that produces one.

src/compiler/flx_core/flx_types.ml

@@ -27,7 +27,7 @@ type recstop = {
   constraint_overload_trail: bid_t list;
   idx_fixlist: bid_t list;
   type_alias_fixlist: (bid_t * int) list;
-  as_fixlist: (string * int) list;
+  as_fixlist: (string * (int * Flx_kind.kind)) list;
   expr_fixlist: (expr_t * int) list;
   depth: int;
   open_excludes: (ivs_list_t * qualified_name_t) list;

src/compiler/flx_desugar/flx_sex2flx.ml

@@ -139,9 +139,10 @@ print_endline ("sex2flx:type] " ^ Sex_print.string_of_sex x);
   | Lst [Id "typ_typeset"; sr; Lst ts] ->
     `TYP_typeset (List.map ti ts)
 
-  | Lst [Id "typ_as"; sr; Lst[t;id]] -> 
+  | Lst [Id "typ_as"; sr; Lst[t;id;knd]] -> 
     let sr = xsr sr in
-    `TYP_as (ti t, xid id)
+    let k = kind_of_sex sr knd in
+    `TYP_as (ti t, xid id, k)
 
   | Lst [Id "typ_apply";  sr; Lst [e1; e2]] -> `TYP_apply(ti e1, ti e2)
   | Lst [Id "typ_type_tuple";  sr; Lst es] -> `TYP_type_tuple (map ti es)

src/packages/control.fdoc

@@ -22,9 +22,14 @@ open class Control
 {
   open C_hack;
 
-  // FIXPOINT OPERATOR
+  // FIXPOINT OPERATORS
+  // For functions
   fun fix[D,C] (f:(D->C)->D->C) (x:D) : C => f (fix f) x;
 
+  // for functors TYPE->K only, the K *must* be specified
+  typefun tfix<K> (f: TYPE->K):K => f x as x:K;
+
+
   /* Example use: factorial function
   fun flat_fact (g:int->int) (x:int):int =>
     if x == 0 then 1 

src/packages/grammar.fdoc

@@ -74,6 +74,7 @@ syntax types {
   k[sarrow_pri] := k[>sarrow_pri] "->" k[sarrow_pri] =># "`(knd_arrow (,_1 ,_3))";
   k[sproduct_pri] := k[>sproduct_pri] ("*" k[>sproduct_pri])+ =># "(chain 'knd_tuple _1 _2)" note "mul";
   k[satomic_pri] := katom =># "_1";
+  k[satomic_pri] := "(" skindexpr ")"  =># "_2";
   katom := sname =># "`(knd_name ,_1)";
   skindexpr_comma_list = list::commalist1<skindexpr>;
 
@@ -88,7 +89,8 @@ syntax types {
     `(typ_typefun ,_sr ,_2 ,_4 ,_6)
     """;
 
-  t[sas_expr_pri] := t[sas_expr_pri] "as" sname =># "`(typ_as ,_sr (,_1 ,_3))";
+  t[sas_expr_pri] := t[sas_expr_pri] "as" sname =># '`(typ_as ,_sr (,_1 ,_3 (knd_name "TYPE")))';
+  t[sas_expr_pri] := t[sas_expr_pri] "as" sname ":" skindexpr =># "`(typ_as ,_sr (,_1 ,_3 ,_5))";
 
   t[stuple_pri] := stypeexpr ("," stypeexpr )+ =># "(chain 'typ_type_tuple _1 _2)";