[Haskell-cafe] Displaying infered type signature of 'offside' functions

[kahl at cas.mcmaster.ca]

Jules Bean <jules at jellybean.co.uk> wrote,
concerning the problem of getting at the types of local definitions:

 > Simon Peyton-Jones wrote:
 > The principal difficulties here are to do with "what do we want"
 > rather the implementation challenges.
 >
 > > 1.  Should the compiler print the type of every declaration? Should GHCi allow you to ask the type of a local decl?
 > >   
 > 
 > IMO, ghci should definitely allow you to ask. This comes up for me every 
 > time that I write any haskell code (and in general I end up hoisting 
 > local definitions to the top level, which is a real pain if there is 
 > local scope, data or type, to hoist with it).
 > 
 > > 2.  How should the variables be identified?  There may be many local bindings for 'f', so you can't say just ":t f".  Ditto if dumping all local bindings.
 > >
 > >   
 > 
 > I think this is a hard question. I was imagining some kind of 
 > hierarchical system like foo.f, in the case that f is locally defined 
 > inside foo. (Yes I know we can't easily use '.' for that). There might 
 > be might be multiple fs inside the definition of foo; indeed there might 
 > even be multiple fs nested inside each other.


I just wanted to contribute a PRACTICAL TRICK I use:


* If the local definition is a pattern binding

    f = ...

  then I just add

    f :: Ordering

* If the local definition is a, say binary, function binding

    f p1 p2 = ...

  then I just add

    f :: Float -> Double -> Ordering

  (Type does not matter for the number of function arrows you need to put;
   only the syntactic arity of the bindings matters here.)


This relies on the fact that the types Float, Double, and Ordering
very rarely occur in my code --- pick your own.


Now the compiler gives you wonderful error messages
``cannot match type `x y z' against Ordering'' ---
so you replace ``Ordering'' with ``x y z''.

If there are type variables in ``x y z''
that come from the context,
take care that you have

{-# LANGUAGE ScopedTypeVariables #-}

at the beginning of your module
(after the {-# OPTIONS ...#-} line,
 which should, as a matter of style,
 NOT contain -fglasgow-exts
)
and the necessary ``forall ty1 ty2 ...'' in front of your the type
in the type signature of the enclosing definition.


At the cost of a re-compilation, this works wonderfully for me,
and is much less painful than hoisting AND exporting local definitions.




But even I still have some wishes open:

* It would be nice if this worked inside the do-notation, too:

  do x :: Ordering
     x <- m

  (This is curently a syntax error.)

* It would be nice if {-# LANGUAGE ScopedTypeVariables #-}
  brought in no other extensions,
  and if GHC would recommend
  the appropriate LANGUAGE pragmas instead of -fglasgow-exts
  when it determines that the user might have wanted some extension.

  (What is the right Language.Extension for GADTs?)



Wolfram