Type-based compilation of everything + fix for #264

[jespercockx]

This PR continues on the path that @flupe has started with #270 and pushes type-based compilation to every corner of agda2hs. It also fixes #264 by removing the horrible compileTopLevelType function and introducing a better way to handle explicit foralls.

Ignoring a number of refactorings, this PR makes the following semantic changes to agda2hs:

• Parameters of data and record types and of type aliases are now compiled according to their type rather than their hiding/quantity annotations. In particular, hidden data parameters are now supported.
• Instance declarations are now also compiled according to their type, so non-erased hidden fields are now supported.
• The check that unboxed records have a single non-erased field is now type-based, so in particular (visible) fields of type Level, Size, and any type in Prop are now allowed (and dropped during compilation).
• Non-erased module parameters are now allowed. Type parameters are turned into explicit foralls to each top-level function in the module, while other parameters are compiled as normal arguments.

The test suite passes and I have added some minimal extra tests, but it could definitely still use some more testing, so please let me know if you have any examples you'd like me to try.

[jespercockx]

One current limitation is that you cannot have where declarations with foralls in their type signature. In fact, if you try to do that by using a module inside your where block, the definitions in that block simply get dropped. For example,

module _ {a : Set} where
  f1 : a → a
  f1 x = f2 id
    where module _ {b : Set} where
      f2 : (a → b) → b
      f2 g = f3 (g x)
        where module _ {c : Set} where
          f3 : c → c
          f3 x = x
      
{-# COMPILE AGDA2HS f1 #-}

is compiled to the rather sad

f1 : forall a . a -> a
f1 x = f2 id

The reason why the definitions of f2 and f3 are dropped is nothing new: it is a consequence of our imperfect attempt at reconstructing the information of which definitions belong to which clause. We use the function isFatherModuleOf (

agda2hs/src/Agda2Hs/AgdaUtils.hs

Lines 41 to 42 in 0611268

	isFatherModuleOf :: ModuleName -> ModuleName -> Bool
	isFatherModuleOf m = maybe False (mnameToList m ==) . initMaybe . mnameToList

) which only considers direct submodules but not indirect ones.

[flupe]

Very nice! I have more questions than remarks really, have yet to think of more tests to add.