Finally get generic functor composition to work.

src/compiler/flx_bind/flx_bind_bexe.ml

@@ -786,26 +786,31 @@ print_endline ("Flx_bind_bexe: UNIFICATION DONE, result= " ^ string_of_bool ures
           index
           parent_ts
       in
+(* NOTE: this shoud already be done.... *)
+      let lhst = Flx_beta.beta_reduce "flx_bind_bexe: EXE_init" state.counter bsym_table sr lhst in
+(*
+print_endline ("Beta reduced LHS is not actually reduced: " ^ sbt bsym_table lhst);
+*)
       let rhst = Flx_fold.minimise bsym_table state.counter rhst in
       if type_match bsym_table state.counter lhst rhst
       then begin 
         let bexe = bexe_init (sr,index,(e',rhst)) in
         [bexe]
       end 
-    else 
-    if ge bsym_table state.counter lhst rhst then
-    let bexe = bexe_init (sr,index,bexpr_coerce ((e',rhst), lhst)) in
-      [bexe]
-    else
-      clierrx "[flx_bind/flx_bind_bexe.ml:782: E30A] " sr
-        (
-          "[bind_exe: init] initialising expression \n" ^
-          sbe bsym_table (e',rhst) ^
-          "\nof type\n" ^
-          sbt bsym_table rhst ^
-          "\nis not a supertype of the declared variable type:\n" ^ 
-          sbt bsym_table lhst 
-        )
+      else 
+        if ge bsym_table state.counter lhst rhst then
+        let bexe = bexe_init (sr,index,bexpr_coerce ((e',rhst), lhst)) in
+          [bexe]
+        else
+          clierrx "[flx_bind/flx_bind_bexe.ml:782: E30A] " sr
+            (
+              "[bind_exe: init] initialising expression \n" ^
+              sbe bsym_table (e',rhst) ^
+              "\nof type\n" ^
+              sbt bsym_table rhst ^
+              "\nis not a supertype of the declared variable type:\n" ^ 
+              sbt bsym_table lhst 
+            )
     end
 
   | EXE_assign (l,r) ->

src/compiler/flx_bind/flx_bind_type.ml

@@ -98,7 +98,7 @@ bind_type'
   bind_type_index
   bind_expression'
   lookup_type_qn_with_sig'
-  lookup_qn_in_env'
+  (lookup_qn_in_env': lookup_state_t -> 'a -> env_t -> 'b -> qualified_name_t -> entry_kind_t * typecode_t list)
   lookup_qn_with_sig'
   state
   bsym_table
@@ -592,13 +592,64 @@ print_endline ("Binding `TYP_name " ^s^ " via params to " ^ sbt bsym_table t);
 (* print_endline ("Trying to bind instancetype"); *)
      btyp_instancetype sr
 
+  | `TYP_fname (sr, name, ks) ->
+(*
+print_endline ("Lookup type function name " ^ name);
+*)
+    let hackname : qualified_name_t  = (`AST_name (sr, name, []) :> qualified_name_t) in
+(*
+print_endline ("Munged qualified name " ^ Flx_print.string_of_qualified_name hackname);
+*)
+    let {base_sym=index; spec_vs=spec_vs; sub_ts=sub_ts} , ts = lookup_qn_in_env' state bsym_table env rs hackname in
+(*
+print_endline ("Found it " ^ name ^ "="^ string_of_int index);
+*)
+    (* we have a problem now: we've found a view of the typefunction, this can happen
+    if the type function is inside a polymorphic class which is opened. The substitution
+    of ts in the view with the vs of the environment must be done, but it cannot be done
+    right now because the type function may not have been bound yet, 
+    but we cannot defer it either, because the BTYP_finst construction only allows
+    for kinding substitutions. We will have to FIXME this later. The type function
+    itself does not support type variable indices, only kind indices.
+    *)
+    let ks = List.map (Flx_btype.bmt "[Flx_bind_type:TYP_fname]") ks in
+    let sym = Flx_sym_table.find state.sym_table index in
+    let dom, cod = match sym.symdef with
+      | SYMDEF_type_function (iks, t) ->
+        (* this constraint requires explicit specification of kind variable bindings.
+           It will be removed when we do kind unification.
+           This has to happen anyhow, in order to kind check the bindings specified
+           produce the correct type function kindings
+           and since this requires unification anyhow, we might as well use
+           the KMGU produced to fix the ks if they're not specified,
+           since we need the KMGU in any case to check, if they are specified,
+           they agree with the infered ones. ... but for now .. hackery
+        *)
+        assert (List.length iks = List.length ks); 
+        begin match t with
+        | `TYP_typefun (kps, cod, body) -> 
+           let dom = match kps with
+           | [] -> KND_tuple [] (* kind unit .. *)
+           | [_,k] -> k
+           | kps -> KND_tuple (List.map snd kps)
+           in dom,cod
+        | _ -> assert false
+        end
+      | _ -> assert false
+    in 
+    let dom = Flx_btype.bmt "Flx_bind_type:bind_type TYP_fname(dom)" dom in 
+    let cod = Flx_btype.bmt "Flx_bind_type:bind_type TYP_fname(cod)" cod in
+    btyp_finst (index, ks, dom, cod)    
+
+  | `TYP_flookup _ ->
+print_endline ("Lookup type function name here");
+     assert false
+
   | `TYP_name _
-  | `TYP_fname _
   | `TYP_case_tag _
   | `TYP_lookup _
-  | `TYP_flookup _
   | `TYP_callback _ as x ->
-      let x =
+      let x : qualified_name_t =
         match qualified_name_of_typecode x with
         | Some q -> q
         | None -> assert false

src/compiler/flx_bind/flx_lookup_type_qn_with_sig.ml

@@ -142,9 +142,6 @@ print_endline ("Lookup type qn with sig, name = " ^ string_of_qualified_name qn)
   | `AST_callback (sr,qn) ->
     failwith "[lookup_type_qn_with_sig] Callbacks not implemented yet"
 
-  | `AST_fname _ ->
-    failwith "[lookup_type_qn_with_sig] `AST_fname not implemented yet"
-
   | `AST_flookup _ ->
     failwith "[lookup_type_qn_with_sig] `AST_flookup not implemented yet"
 
@@ -191,6 +188,20 @@ print_endline ("Lookup type qn with sig, name = " ^ string_of_qualified_name qn)
       sra srn
       env env rs name ts signs
 
+  | `AST_fname (sr, name, ks) ->
+    print_endline ("lookup_type_qn_with_sig': AST_fname " ^ name ^ " calling lookup_type_name_with_sig");
+    let t =
+      lookup_type_name_with_sig
+      state
+      bsym_table
+      sra srn
+      env env rs name [] signs
+    in
+    print_endline ("Got type: " ^ Flx_print.sbt bsym_table t);
+    assert false
+
+
+
   | `AST_index (sr,name,index) as x ->
     print_endline ("[lookup_type_qn_with_sig] AST_index " ^ string_of_qualified_name x);
     begin match get_data state.sym_table index with

src/compiler/flx_core/flx_ast.ml

@@ -66,6 +66,8 @@ and kindcode_t =
   | KND_tuple of kindcode_t list
   | KND_tpattern of typecode_t
   | KND_special of string
+  | KND_var of string
+
 
 and sortcode_t = 
   | SRT_kind

src/compiler/flx_core/flx_btype.ml

@@ -927,13 +927,13 @@ let rec bmt msg mt = match mt with
   | Flx_ast.KND_bool -> kind_bool
   | Flx_ast.KND_function (t1,t2) -> kind_function (bmt msg t1, bmt msg t2)
   | Flx_ast.KND_tuple(ts) -> kind_tuple(List.map (bmt msg) ts)
-  | _ -> kind_type 
-(*
-  | Flx_ast.KND_tpattern t -> print_endline ("BMT tpattern fail " ^ msg); assert false
+  | Flx_ast.KND_var s -> kind_var s
+
+  (* this is wrong, we actually need to examine the pattern to find the kind *)
+  | Flx_ast.KND_tpattern t -> kind_type (*  print_endline ("BMT tpattern fail " ^ msg); assert false *)
   | Flx_ast.KND_typeset ts -> print_endline ("BMT typeset fail " ^ msg); assert false 
-  | Flx_ast.KND_generic -> print_endline ("BMT generic fail " ^ msg); assert false
+  | Flx_ast.KND_generic -> kind_type (* requied at least for GADTs to work *) 
   | Flx_ast.KND_special s -> print_endline ("BMT special fail " ^ msg); assert false
-*)
 
 (* -------------------------------------------------------------------------- *)
 
@@ -1028,7 +1028,7 @@ let reduce_typeop op t k =
 
 (** Recursively iterate over each bound type and transform it with the
  * function. *)
-let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) = function
+let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) ?(f_kind=fun k->k) = function
   | BBOOL v -> bbool v
   | BTYP_typeof (i,t) -> btyp_typeof (f_bid i, t)
   | BTYP_typeop (op,t,k) -> btyp_typeop op (f_btype t) k
@@ -1046,8 +1046,8 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) = function
     | _ -> BTYP_sum (Flx_list.repeat mapped_unit k)
     end
   | BTYP_inst (it,i,ts,mt) -> btyp_inst (it,f_bid i, List.map f_btype ts,mt)
-  | BTYP_finst (i,ks,dom,cod) -> btyp_finst (f_bid i, ks, dom,cod)
-  | BTYP_vinst (i,ts,mt) -> btyp_vinst (f_bid i, List.map f_btype ts,mt)
+  | BTYP_finst (i,ks,dom,cod) -> btyp_finst (f_bid i, List.map f_kind ks, f_kind dom, f_kind cod)
+  | BTYP_vinst (i,ts,mt) -> btyp_vinst (f_bid i, List.map f_btype ts,f_kind mt)
   | BTYP_intersect ts -> btyp_intersect (List.map f_btype ts)
   | BTYP_tuple ts -> btyp_tuple (List.map f_btype ts)
   | BTYP_compacttuple ts -> btyp_compacttuple (List.map f_btype ts)
@@ -1077,13 +1077,13 @@ let rec map ?(f_bid=fun i -> i) ?(f_btype=fun t -> t) = function
   | BTYP_borrowed t -> btyp_borrowed (f_btype t)
 
   | BTYP_void as x -> x
-  | BTYP_fix _ as x -> x
+  | BTYP_fix (i,k) -> btyp_fix i (f_kind k)
   | BTYP_tuple_cons (a,b) -> btyp_tuple_cons (f_btype a) (f_btype b)
   | BTYP_tuple_snoc (a,b) -> btyp_tuple_snoc (f_btype a) (f_btype b)
   | BTYP_type_tuple ts -> btyp_type_tuple (List.map f_btype ts)
   | BTYP_type_function (its, a, b) ->
-      btyp_type_function (List.map (fun (i,t) -> f_bid i,t) its, a, f_btype b)
-  | BTYP_type_var (i,t) -> btyp_type_var (f_bid i,t)
+      btyp_type_function (List.map (fun (i,k) -> f_bid i,f_kind k) its, f_kind a, f_btype b)
+  | BTYP_type_var (i,k) -> btyp_type_var (f_bid i,f_kind k)
   | BTYP_type_apply (a, b) -> btyp_type_apply (f_btype a, f_btype b)
   | BTYP_type_map (a, b) -> btyp_type_map (f_btype a, f_btype b)
   | BTYP_type_match (t,ps) ->

src/compiler/flx_core/flx_btype.mli

@@ -207,7 +207,7 @@ val flat_iter :
 val iter :
   ?f_bid:(bid_t -> unit) -> ?f_btype:(t -> unit) -> t -> unit
 val map :
-  ?f_bid:(bid_t -> bid_t) -> ?f_btype:(t -> t) -> t -> t
+  ?f_bid:(bid_t -> bid_t) -> ?f_btype:(t -> t) -> ?f_kind:(Flx_kind.kind -> Flx_kind.kind) -> t -> t
 val contains_uniq: t -> bool
 val adjust_fixpoint: t -> t
 val widen_fixgap : int -> t -> t

src/compiler/flx_core/flx_btype_kind.ml

@@ -3,8 +3,11 @@ open Flx_exceptions
 open Flx_kind
 
 let rec metatype sr term : kind =
+try
   let t = metatype' sr term in
   t
+with exn -> print_endline ("Mt FAIL " ^ Printexc.to_string exn);
+ assert false
 
 and metatype' sr typ : kind =
   let st t = Flx_btype.st t in
@@ -21,16 +24,32 @@ and metatype' sr typ : kind =
     kind_max (List.map (fun (_,t) -> mt t) bs)
 
   | BTYP_type_function (a,r,body) ->
+(*
+print_endline ("Meta type of type function .. return kind " ^ Flx_kind.sk r);
+*)
     let ps = List.map snd a in
     let argt =
       match ps with
       | [x] -> x
       | _ -> kind_tuple ps
     in
+(*
+print_endline ("Meta type of type function .. parameter kind " ^ Flx_kind.sk argt);
+*)
     let bk =  mt body in
+(*
+let _ = print_endline ("Meta type of type function body " ^ Flx_kind.sk bk) in
+*)
     if kind_ge2 r bk then
-      kind_function (argt,r)
+      let k = kind_function (argt,r) in
+(*
+      let _ = print_endline (" ** RESULT " ^ Flx_kind.sk k) in
+*)
+      k
     else 
+(*
+      let _ = print_endline ("Metatype error, function body kind isn't subkind of return kind") in
+*)
       clierrx "[Flx_btype_kind:32: E239] " sr
         (
           "Flx_btype_kind: In type function \n" ^

src/compiler/flx_core/flx_btype_subst.ml

@@ -139,18 +139,9 @@ let varmap_of_mgu mgu =
   List.iter (fun (varidx, typ) -> Hashtbl.add varmap varidx typ) mgu;
   varmap
 
-
 let tsubst sr (vs:Flx_kind.bvs_t) ts t =
   varmap_subst (mk_varmap sr vs ts) t
 
-let ksubst sr (bks:Flx_kind.bks_t) ks t =
-  if List.length bks <> List.length ks then assert false;
-  if List.length bks <> 0 then begin
-    print_endline ("Flx_btype.ksubst (kind variable substitution) not implemented yet");
-    assert false
-  end;
-  t
-
 let neuter_polyrecs msg t = 
   let rec aux t = 
     match Flx_btype.map ~f_btype:aux t with

src/compiler/flx_core/flx_expand_typedef.ml

@@ -6,7 +6,7 @@ let rec find_in_list counter t lst =
      if Flx_typeeq.type_eq (Flx_btype.st) counter h t then Some i else
      find_in_list counter t tail
 
-let rec expand bsym_table  counter sr t =
+let rec expand bsym_table  counter sr (t:Flx_btype.t):Flx_btype.t = 
 (*
 print_endline ("EXPAND " ^ Flx_print.sbt bsym_table t);
 *)
@@ -72,7 +72,7 @@ print_endline ("processed ts = " ^ catmap "," Flx_btype.st ts);
 *)
         end
 
-      | BTYP_finst (index,ks,dom,cod) ->
+      | BTYP_finst (index,ks,dom,cod) -> 
         begin try
           let bsym = Flx_bsym_table.find bsym_table index in
           let bbdcl = Flx_bsym.bbdcl bsym in
@@ -81,13 +81,21 @@ print_endline ("processed ts = " ^ catmap "," Flx_btype.st ts);
 (*
         print_endline ("EXPANDING FUNCTION "^bsym.id^" INSTANCE");
 *)
-            let salias = Flx_btype_subst.ksubst sr bks ks alias in (* kind variable substitution *)
-            aux ((t,level)::trail) level salias (* NO level increment *)
+            let ksubst (knd:Flx_kind.kind):Flx_kind.kind = Flx_kind.ksubst sr bks ks knd in
+            let rec f_btype t = Flx_btype.map ~f_btype ~f_kind:ksubst t in
+            let alias = f_btype alias in
+(*
+print_endline ("Flx_expand_typedef: expanded type function with kind subs  =\n **** " ^ Flx_print.sbt bsym_table t);
+*)
+            begin match alias with
+            | BTYP_type_function _ ->
+              aux ((t,level)::trail) level alias (* NO level increment *)
+            | _ -> assert false
+            end
           | _ -> assert false
           end
         with Not_found -> assert false
         end
-
       | _ -> Flx_btype.map ~f_btype:(aux (trail) (level+1)) t
   in
 (*
@@ -106,4 +114,3 @@ print_endline ("processed ts = " ^ catmap "," Flx_btype.st ts);
 (*
   end
 *) 
-