[TYPES] seeking correct term for a quasi-dependent type

[Norman Ramsey]

A new feature of the Glasgow Haskell Compiler, called 'indexed type
families', makes it possible to write something that isn't a true
dependent type but isn't parametrically polymorphic either.
I'd like help figuring out what to call it.  Here's an
example that is pretty close to what we're actually doing:

  outputFact :: forall a . a -> Info a

Although 'Info' has the same syntax as a parametric type
*constructor*, it is actually a *partial* *function* on types:

  data Fact   = ...
  data Middle = ...
  data Last   = ...
  newtype Label = Label Int

  -- here follows the definition of 'Info':
  type family   Info a :: *
  type instance Info Middle = Fact
  type instance Info Last   = [(Label, Fact)]

How do I describe the function 'outputFact'?
It's not a classic dependent function, because the type of the result
doesn't depend on the value of the argument.  But the type of the
result *does* depend on the static *type* of the argument.

And outputFact is less polymorphic than it might appear, since the
bound type variable 'a' cannot be instantiated at any type, but only
at a type in the domain of the type function 'Info'.

I'm a little reluctant to call 'outputFact' a "dependent function"
or to say that it has a "dependent-function type", because those
words mean something else.  But I'm at a loss as to how to describe it.

What sort of type is the type 

  forall a . a  -> Info a  

?



Norman