I too miss the old way of handling local type variables. Previously, local type annotations worked a lot like an additional constraint, with type variables denoting some type. The same type variable denoted the same type. Here's how it works in OCaml, for example: # let pair x y = (x,y);; val pair : 'a -> 'b -> 'a * 'b = <fun> # let pair1 (x:'a) (y:'a) = (x,y);; val pair1 : 'a -> 'a -> 'a * 'a = <fun> # let pair2 x y = ((x:'a),(y:'a));; val pair2 : 'a -> 'a -> 'a * 'a = <fun> # let pair3 x (y:int) = ((x:'a),(y:'a));; val pair3 : int -> int -> int * int = <fun> # let pair4 x (y:int) = ((x:'a list),(y:'a));; val pair4 : int list -> int -> int list * int = <fun> # let pair5 (x:'a list) (y:int) = (x,(y:'a));; val pair5 : int list -> int -> int list * int = <fun> Which of the two occurrences of the type variable |'a| a binding one? Who cares... It just works: within the same expression, the same type variable stands for the same type.
I'm looking for some tips and references regarding prescribing poly-/mono-morphism. I know of three ways to do it: 1) rely on the monomorphism-restriction -- kind of scary in that its not explicitly obvious 2) introducing scoped-type variables of interest -- explicit and modular 3) introducing all type variables with a forall -- explicit but not modular
It seems that with GCH 6.6, we are forced to go back to the fourth method -- the one that was available back in Haskell98. Use useless expressions to hint the typechecker.
bop :: forall x y z m c v . ( SubType x v, SubType y v, SubType z v , SubType (Fun m c v) v , Monad m, Comonad c ) => (x -> y -> z) -> Fun m c v bop op = Fun fn where fn = wrap fn' where fn' v0 = (inj . Fun) (wrap fn'') where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj v1) wrap :: (v -> v) -> (c v -> m v) wrap = (return .) . (. counit) If I leave the types to inference (i.e. drop the forall and the type ascription for |wrap|), then I end up with this type
bop :: ( SubType x v2, SubType y v1, SubType z v1 , SubType (Fun m c v1) v2 , Monad m, Comonad c ) => (x -> y -> z) -> Fun m c v2 Note the multiple |v|s; they wreak havoc in the rest of my code.
It seems that you wish that, for example, v0 and v1 be of the same type. We have to be direct then and write where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj (v1 `asTypeOf` v0) or where fn'' v1 = inj (lazyPrj v0 `op` lazyPrj v1) where useless = if True then v0 else v1 or where fn'' v1 | const True [v0,v1] = inj (lazyPrj v0 `op` lazyPrj v1) or something similar...