So that happened....

yep.ur

datatype notlist a = NotNil | NotCons of (a * notlist a)

structure Pointed : sig
  class pointed :: (Type -> Type) -> Type
  val point : a ::: Type -> f ::: (Type -> Type)
              -> pointed f
              -> a -> f a

  val mkPointed : f ::: (Type -> Type)
                  -> {Point : a ::: Type -> a -> f a}
                  -> pointed f
end = struct
  con pointed f = {Point : a ::: Type -> a -> f a}
  fun point [a] [f] (witness : pointed f) = @@witness.Point [a]
  fun mkPointed [f] witness = witness
end
structure Hunctor : sig
  class hunctor :: (Type -> Type) -> Type
  val fmap : a ::: Type -> b ::: Type -> f ::: (Type -> Type)
             -> hunctor f
             -> (a -> b)
             -> f a
             -> f b
  val mkHunctor : f ::: (Type -> Type)
                  -> {Fmap : a ::: Type -> b ::: Type -> (a -> b) -> f a -> f b}
                  -> hunctor f
end = struct
  con hunctor f = {Fmap : a ::: Type -> b ::: Type -> (a -> b) -> f a -> f b}
  fun fmap [a] [b] [f] (witness : hunctor f) = @@witness.Fmap [a] [b]
  fun mkHunctor [f] witness = witness
end

open Pointed
open Hunctor

val pointed_list : pointed list = mkPointed {Point = fn [a] x => Cons (x,Nil)}
val hunctor_list : hunctor list = mkHunctor {Fmap = fn [a] [b] => List.mp}