Fwd: Decomposition of given equalities

[Thijs Alkemade]

[Resending to the list, I used the wrong address. Sorry for the duplicate 
copies.]

On 19 dec. 2013, at 05:30, Richard Eisenberg  wrote:

> I'd say GHC has it right in this case.
> 
> (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds 
> match up. If, say, (f :: k1 -> *), (g :: k2 -> *), (a :: k1), and (b :: k2), 
> then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's initial problem, we have 
> (with all type, kind, and coercion variables made explicit)

But even when it can know the kinds match up it doesn’t decompose it. For 
example:

—

{-# LANGUAGE TypeFamilies #-}

foo :: (f a ~ g b) => f a -> g b
foo = id

—

Ends up with 2 errors (7.6.3):

   Could not deduce (a ~ b)
   from the context (f a ~ g b)

   Could not deduce (f ~ g)
   from the context (f a ~ g b)

So the wanted constraint f a ~ g b was decomposed, meaning the kind of a and b, 
and f and g were already found to be equal. Even with an explicit kind 
signature on every variable it doesn't work:

foo :: (f a ~ g b) => (f :: * -> *) (a :: *) -> (g :: * -> *) (b :: *)

I can’t think of an example where f a ~ g b holds, but the kinds of a and b are 
different.

Thijs (“xnyhps”)



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Error building ghc on raspberry pi.

[Thijs Alkemade]

Op 15 jan. 2013, om 18:16 heeft Karel Gardas  het 
volgende geschreven:

> Well, if you make some board available in DMZ I'm certainly interested to run 
> at least configure on it from GHC HEAD to see what we need to hack in order 
> to add support for RPi into GHC HEAD.
> 
> Unfortunately GHC HEAD is now in a wrong state w.r.t. LLVM based build, but 
> Austin is working on this. I think I can hack support for RPi in the meantime 
> for testing later on fixed GHC HEAD LLVM build...
> 
> Karel

This might be helpful, it's a guide to emulate a raspberry pi using qemu, which 
I was using to (try to) build GHC:

http://xecdesign.com/qemu-emulating-raspberry-pi-the-easy-way/

While I haven't done any real measurements, it seemed somewhat faster too on my 
machine.

Thijs
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Error building ghc on raspberry pi.

[Thijs Alkemade]

Op 15 jan. 2013, om 17:36 heeft rocon...@theorem.ca het volgende geschreven:

> Okay, I tried:
> 
> SRC_HC_OPTS= -H64m -Rghc-timing -optc-mfloat-abi=hard 
> -optc-march=armv6 -optc-mfpu=vfp -optlc=-mattr=+vfp2
> GhcStage1HcOpts= -O -fllvm
> GhcStage2HcOpts= -O0 -fllvm
> GhcLibHcOpts   = -O -fllvm -optlc-float-abi=hard
> 
> and I got the same error at a different build step.  I'm not sure if it is 
> earlier or later.
> 
> It seems still not everything is using the hard-float ABI.
> 
> ===--- building final phase
> make -r --no-print-directory -f ghc.mk phase=final all
>  HC [stage 1] utils/hsc2hs/dist-install/build/tmp/hsc2hs
> /usr/bin/ld: error: utils/hsc2hs/dist-install/build/tmp/hsc2hs uses VFP 
> register arguments, utils/hsc2hs/dist-install/build/Main.o does not
> /usr/bin/ld: failed to merge target specific data of file 
> utils/hsc2hs/dist-install/build/Main.o
...

Did you do a `make clean` first? If not, try removing just (some of) the 
offending .o files, and see if rebuilding just those results in the same error.

Thijs
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Error building ghc on raspberry pi.

[Thijs Alkemade]

Op 14 jan. 2013, om 17:30 heeft rocon...@theorem.ca het volgende geschreven:

> On Thu, 10 Jan 2013, Karel Gardas wrote:
> 
>> 
>> Hmm, are you using Raspbian? I.e. hard-float abi caught my eye in case of 
>> ARMv6/ARM11 chip here...
>> 
>> I'm afraid LLVM is not well guided in your case so could you be so kind and 
>> test if adding -optlc=-mattr=+vfp2 helps? You need to add it to your 
>> build.mk probably and you will need to rebuild everything again...
> 
> No change with
> 
> SRC_HC_OPTS= -H64m -Rghc-timing -optc-mfloat-abi=hard 
> -optc-march=armv6 -optc-mfpu=vfp -optlc=-mattr=+vfp2
> GhcStage1HcOpts= -O -fllvm
> GhcStage2HcOpts= -O0 -fllvm
> GhcLibHcOpts   = -O -fllvm
> 
> I still get the error:
> 
> ===--- building final phase
> make -r --no-print-directory -f ghc.mk phase=final all
>  LD libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o
> /usr/bin/ld: error: libraries/ghc-prim/dist-install/build/cbits/debug.o uses 
> VFP register arguments, 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o does not
> /usr/bin/ld: failed to merge target specific data of file 
> libraries/ghc-prim/dist-install/build/cbits/debug.o
> 
> I don't really understand what is going on here.  The file 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o doesn't even 
> exist, so when I manually run /usr/bin/ld I get:
> 
> $ /usr/bin/ld libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o
> /usr/bin/ld: cannot find 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o: No such file or 
> directory
> 
> What is make really doing here?
> 
> My research suggests that this error is a symptom of trying to link something 
> without the hard-float ABI together with something with a soft-float ABI.  
> But I don't know where 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o is coming from.

libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o is the output ld was 
asked to generate. Apparently, some of the input .o files didn't use VFP 
register arguments, so ld concluded that the output should also not use VFP 
register arguments. But then ld encountered a .o file that did use VFP register 
arguments, and threw an error (something in cbits, so probably built with 
different CFLAGS).

>From your flags I'd say you miss -optlc-float-abi=hard. I had it in 
>GhcLibHcOpts, but I'm not sure that is the correct way to ensure it is passed 
>to everything exactly once.

Thijs
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Error building ghc on raspberry pi.

[Thijs Alkemade]

Op 8 jan. 2013, om 05:16 heeft rocon...@theorem.ca het volgende geschreven:

> On Thu, 3 Jan 2013, Thijs Alkemade wrote:
> 
>> I believe I had the same problem, which disappeared after upgrading llvm 
>> from 3.0 to 3.1, and using that instead for ./configure.
>> 
>> Hope this helps,
>> Thijs
> 
> Thanks, using LLVM 3.1 seems to have improved the siutation, but I'm running 
> into a new error.
> 
> Here is the error I get when trying to build GHC 7.6.1 from 7.4.1
> 
> ===--- building final phase
> make -r --no-print-directory -f ghc.mk phase=final all
>  LD libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o
> /usr/bin/ld: error: libraries/ghc-prim/dist-install/build/cbits/debug.o uses 
> VFP register arguments, 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o does not
> /usr/bin/ld: failed to merge target specific data of file 
> libraries/ghc-prim/dist-install/build/cbits/debug.o
> /usr/bin/ld: error: libraries/ghc-prim/dist-install/build/cbits/longlong.o 
> uses VFP register arguments, 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o does not
> /usr/bin/ld: failed to merge target specific data of file 
> libraries/ghc-prim/dist-install/build/cbits/longlong.o
> /usr/bin/ld: error: libraries/ghc-prim/dist-install/build/cbits/popcnt.o uses 
> VFP register arguments, 
> libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o does not
> /usr/bin/ld: failed to merge target specific data of file 
> libraries/ghc-prim/dist-install/build/cbits/popcnt.o
> make[1]: *** [libraries/ghc-prim/dist-install/build/HSghc-prim-0.3.0.0.o] 
> Error 1
> 
> I get similar errors when building GHC 7.4.1 (patched with 
> http://hackage.haskell.org/trac/ghc/attachment/ticket/5914/0001-add-support-for-ARM-hard-float-ABI-fixes-5914.patch).
> 
> Any of you encountered this problem before?
> 

Yeah, I had a lot of these. The problem was that GHC has a lot of different 
"CFLAGS",
so finding the right way to pass "-float-abi=hard" to every one of them took 
some time, but
eventually I ended up with the following change to mk/build.mk:

ifeq "$(BuildFlavour)" "quick"

SRC_HC_OPTS= -H64m -O0 -fasm
GhcStage1HcOpts= -O -fasm
GhcStage2HcOpts= -O0 -fasm
GhcLibHcOpts   = -O -fasm -optlc-float-abi=hard
SplitObjs  = NO
HADDOCK_DOCS   = NO
BUILD_DOCBOOK_HTML = NO
BUILD_DOCBOOK_PS   = NO
BUILD_DOCBOOK_PDF  = NO

endif

(Change the build flavor you are using, of course)

And I ran configure as:

LDFLAGS="-marm -mfloat-abi=hard -mfpu=vfp" CFLAGS="-marm -mfloat-abi=hard 
-mfpu=vfp" ./configure --with-opt=/usr/bin/opt-3.1 --with-llc=/usr/bin/llc-3.1 
--with-ld=`which ld.gold`

(I switched to the gold linker, because ld was running out of RAM often.)

I did eventually finish building stage2, but the final executable segfaulted on 
start.
I haven't investigated much why that happened, the days it takes to rebuild it 
just
made me give up.

Hope this helps,
Thijs
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Error building ghc on raspberry pi.

[Thijs Alkemade]

(Sorry, forgot to CC the list)


 Original Message 
From: Thijs Alkemade 
Sent: Thu Jan 03 10:31:50 CET 2013
To: rocon...@theorem.ca
Subject: Re: Error building ghc on raspberry pi.

rocon...@theorem.ca wrote:

>Some further information it seems that llc is segfaulting:
>
>pi@raspberrypi /tmp/ghc-7.4.1 $ llc -O3 -relocation-model=static
>/tmp/ghc7189_0/ghc7189_0.bc -o /tmp/ghc7189_0/ghc7189_0.lm_s 
>Stack dump:
>0.  Program arguments: llc -O3 -relocation-model=static
>/tmp/ghc7189_0/ghc7189_0.bc -o /tmp/ghc7189_0/ghc7189_0.lm_s 
>1.  Running pass 'Function Pass Manager' on module
>'/tmp/ghc7189_0/ghc7189_0.bc'.
>2.  Running pass 'ARM Instruction Selection' on function
>'@ghczmprim_GHCziTypes_Czh_info'
>Segmentation fault
>pi@raspberrypi /tmp/ghc-7.4.1 $ llc --version
>Low Level Virtual Machine (http://llvm.org/):
>   llvm version 3.0
>(Debian 3.0-10)Optimized build.
>   Built Jul 26 2012 (20:20:52).
>   Host: arm-unknown-linux-gnueabihf
>   Host CPU: (unknown)
>
>   Registered Targets:
> alpha- Alpha [experimental]
> arm  - ARM
> bfin - Analog Devices Blackfin [experimental]
> c- C backend
> cellspu  - STI CBEA Cell SPU [experimental]
> cpp  - C++ backend
> mblaze   - MBlaze
> mips - Mips
> mips64   - Mips64 [experimental]
> mips64el - Mips64el [experimental]
> mipsel   - Mipsel
> msp430   - MSP430 [experimental]
> ppc32- PowerPC 32
> ppc64- PowerPC 64
> ptx32- PTX (32-bit) [Experimental]
> ptx64- PTX (64-bit) [Experimental]
> sparc- Sparc
> sparcv9  - Sparc V9
> systemz  - SystemZ
> thumb- Thumb
> x86  - 32-bit X86: Pentium-Pro and above
> x86-64   - 64-bit X86: EM64T and AMD64
> xcore- XCore
>
>On Wed, 2 Jan 2013, rocon...@theorem.ca wrote:
>
>> I'm trying to build ghc-7.4.1 using ghc-7.4.1 on my raspberry pi
>(armv6l) and 
>> I get the following error:
>>
>> "inplace/bin/ghc-stage1"   -H32m -O-package-name ghc-prim-0.2.0.0
>
>> -hide-all-packages -i -ilibraries/ghc-prim/. 
>> -ilibraries/ghc-prim/dist-install/build 
>> -ilibraries/ghc-prim/dist-install/build/autogen 
>> -Ilibraries/ghc-prim/dist-install/build 
>> -Ilibraries/ghc-prim/dist-install/build/autogen
>-Ilibraries/ghc-prim/. 
>> -optP-include 
>> -optPlibraries/ghc-prim/dist-install/build/autogen/cabal_macros.h
>-package 
>> rts-1.0  -package-name ghc-prim -XHaskell98 -XCPP -XMagicHash 
>> -XForeignFunctionInterface -XUnliftedFFITypes -XUnboxedTuples 
>> -XEmptyDataDecls -XNoImplicitPrelude -O2  -no-user-package-conf
>-rtsopts 
>> -odir libraries/ghc-prim/dist-install/build -hidir 
>> libraries/ghc-prim/dist-install/build -stubdir 
>> libraries/ghc-prim/dist-install/build -hisuf hi -osuf  o -hcsuf hc -c
>
>> libraries/ghc-prim/./GHC/Types.hs -o 
>> libraries/ghc-prim/dist-install/build/GHC/Types.o
>> Stack dump:
>> 0.  Program arguments: llc -O3 -relocation-model=static 
>> /tmp/ghc6324_0/ghc6324_0.bc -o /tmp/ghc6324_0/ghc6324_0.lm_s 1. 
>Running 
>> pass 'Function Pass Manager' on module '/tmp/ghc6324_0/ghc6324_0.bc'.
>> 2.  Running pass 'ARM Instruction Selection' on function 
>> '@ghczmprim_GHCziTypes_Czh_info'
>> /tmp/ghc6324_0/ghc6324_0.lm_s: openBinaryFile: does not exist (No
>such file 
>> or directory)
>> make[1]: *** [libraries/ghc-prim/dist-install/build/GHC/Types.o]
>Error 1
>> make: *** [all] Error 2
>>
>> Anyone have any thoughts on what might be the matter and what I can
>do to fix 
>> it.  (If only openBinaryFile said which file doesn't exist.)
>>
>>

I believe I had the same problem, which disappeared after upgrading llvm from 
3.0 to 3.1, and using that instead for ./configure.

Hope this helps,
Thijs

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: TypeHoles: unbound variables as named holes

[Thijs Alkemade]

Hey all,

To report on the current situation:

I'm myself still not sure which of the options of sharing/not sharing
is the most useful. I can't really estimate which I would want to use
the most, so I wouldn't dare to predict which most users would want.

However, the module-wide sharing is hard, and as Simon mentioned is
problematic with polymorphism. We've looked at this before, and right
now I think I don't have the time to finish that.

No sharing, the way Simon proposed it, was rather easy to add. What I
have now works like this: When -XTypeHoles is on, any unbound
identifier that starts with _ is also turned into a hole, with an
appropriate message. For example, the module:

f = _a _b _

Gives (these are warnings, because -fdefer-type-errors is on):

---

holes2.hs:1:5: Warning:
Found hole with type: `t0 -> t1 -> t'
Arising from: an undeclared identifier `_a' at holes2.hs:1:5-6
Where: `t0' is an ambiguous type variable
   `t1' is an ambiguous type variable
   `t' is a rigid type variable bound by
   the inferred type of f :: t at holes2.hs:1:1
Relevant bindings include f :: t (bound at holes2.hs:1:1)
In the expression: _a
In the expression: _a _b _
In an equation for `f': f = _a _b _

holes2.hs:1:8: Warning:
Found hole with type: `t0'
Arising from: an undeclared identifier `_b' at holes2.hs:1:8-9
Where: `t0' is an ambiguous type variable
In the first argument of `_a', namely `_b'
In the expression: _a _b _
In an equation for `f': f = _a _b _

holes2.hs:1:11: Warning:
Found hole with type: `t1'
Arising from: a use of `_' at holes2.hs:1:11
Where: `t1' is an ambiguous type variable
In the second argument of `_a', namely `_'
In the expression: _a _b _
In an equation for `f': f = _a _b _

---

I think this is a good compromise that gives you named holes and
easily allows you to turn unbound identifiers into holes. What do you
think?

Regards,
Thijs Alkemade

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Comments on current TypeHoles implementation

[Thijs Alkemade]

On 4 okt. 2012, at 23:33, Roman Cheplyaka  wrote:

> Sounds cool. I would also expect that if you have several occurences of
> the same unbound identifier, then it gets a unified type.
> 

We have actually tried to do it this way for a pretty long time. But it's not 
as 
easy as it sounds. We were hoping to make all holes inside one module 
to be shared and get a unified type, but that turned out to not fit with our 
implementation of holes. Holes are treated as constraints, which apply to 
the type of one function, there's no such thing as a constraint for a whole 
module.

You can also not treat the holes as "fake" top level declarations:

> I guess this is something you can get currently by creating a top-level
> declaration
> 
>  foo = _
> 
> and then using foo in several places.

This example will just result in one hole with type "t". The call locations for 
`foo' have no influence on its type.

If we'd want holes to just be shared within one function, then that is pretty 
easy to do right now. We could turn the definition of a hole in HsExpr into 
`HsHole (Maybe RdrName)' (or whatever String-like type is most 
appropriate), in the renamer, change rnExpr for HsVars to return a hole 
when it can't find it, storing the original name. Then ensure holes with the 
same name interact properly (in canHole), and update the way they are 
printed.

Best regards,
Thijs
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

Hi Simon,

On Tue, Aug 21, 2012 at 7:14 PM, Simon Peyton-Jones
 wrote:
> Can you give me read/write access to your github repo?  I'm simonpj on github.
> That way I can add comments/questions in code, and generally clean up.
> It would make things easier if you could merge with HEAD so that I don't have 
> to mess around moving libraries back in time.

Done. I've merged with HEAD as of right now. The only subrepository
I've forked is the testsuite repository, which you can find on
https://github.com/xnyhps/testsuite.

I've tried to get validate to pass all tests, I had to fix this one:
https://github.com/xnyhps/testsuite/commit/5016899250ace0d2db227569073ad83573909728,
and I've added this
https://github.com/xnyhps/testsuite/commit/47f1bb7f7c8aced6e59f8d3e2413f6c6c5b6016e
as a test case for holes. It's not a very complicated example of
holes, but I'm a bit unsure how to properly write a test case for it.
If you have some ideas to do this better, I'd be interested.

Some other tests were reporting to be too (in)efficient, but compared
to running validate on HEAD without my patch it seemed the same thing
happened there, so I haven't look further into those.

>
> --
> You've put "LANGUAGE Holes" in TcErrors which means I can't bootstrap.
>

Sorry, that was sloppy, I've fixed it.

> --
> You have this in your patch file, which can't be right
> +  | CHoleCan {
> +  cc_ev   :: CtEvidence,
> +  cc_hole_ty  :: TcTauType, -- Not a Xi! See same not as above
> +  cc_depth:: SubGoalDepth-- See Note [WorkList]
> +}
> +
>  \end{code}
>
>  \begin{code}
> @@ -933,6 +940,9 @@ ctPred (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })
>  ctPred (CFunEqCan { cc_fun = fn, cc_tyargs = xis1, cc_rhs = xi2 })
>= mkTcEqPred (mkTyConApp fn xis1) xi2
>  ctPred (CIrredEvCan { cc_ty = xi }) = xi
> +ctPred (CHoleCan { cc_flavor = fl, cc_hole_ty = xi })
> +  = xi
> +
>
> since c_flavor isn't a field of CHoleCan.
>

This code is gone after merging with HEAD.

> ---
>
> | The 3 currently remaining issues:
> |
> | - Free type variables are not tidied consistently. For every one of
> | these hole warnings, the same TidyEnv is reused, without taking the
> | updates from the other holes into account. I'm pretty sure I know where
> | this happens and how I could fix it.
>
> This should be easy.
> * TcErrors.reportUnsolved uses tyVarsOfWC to find the free type variables
>   of unsolved constraints
> * It then uses tidyFreeTyVars to assign them names
> * And that gives an env used in tidying.
>
> So it should just work.  I hope you are letting the various 'tidy' calls in 
> TcErrors do the work.
>

I traced the problem back to not zonking the hole constraint properly,
reporting them now works as it should (I've removed the hack I was
using, and cleaned up some code that didn't need to be monadic
anymore).

(The reason they weren't zonked properly is that I've given zonkCt a
special case for CHoleCans
(https://github.com/xnyhps/ghc/blob/eee4242df72cf0a7910e896c3bd6d0fb20b97e37/compiler/typecheck/TcMType.lhs#L619),
as holes themselves do not carry enough information for me to turn
them from CNonCanonicals back into CHoleCans (they become
CIrredEvCans). I'm still not sure this is the right thing to do here.)

> | - What I thought would be the local environment doesn't actually seem
> | to be it. The holes store in their origin the result of `getLclTypeEnv'
> | at their location, but as the Note [Bindings with closed types] says,
> | the TopLevelFlag of these don't actually differentiate the top level
> | from the non-top level bindings. I think it would be more helpful to
> | only show the non-top level bindings at the hole's location, any hints
> | about how to obtain just these would be appreciated.
>
> In this context "local" means "this module" rather than "not top level".  Use 
> isExternalName to distinguish top-level things from nested things.
>

This works now, thanks!


> | - The holes do not have very accurate source location information, like
> | some other errors have. The hole has its origin, ("test2.hs:3:16"), but
> | somehow not something like: "In the expression: folder _ x _, In an
> | equation for `test': test x = foldr _ x _". Help with how that is
> | supposed to work would also be appreciated.
>
> That's odd.  Every Wanted constraint has a WantedLoc (TcRnTypes), which 
> includes a [ErrCtxt], which is that stack of "In ..; In... " stuff you see.
>
> Code looks plausible.

I've fixed the way I was constructing the CtLoc, this was wrong and
was always using [] as the [ErrCtxt].


Regards,
Thijs Alkemade

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: API function to check whether one type fits "in" another

[Thijs Alkemade]

On 19 jul. 2012, at 19:28, Philip Holzenspies wrote:

> Dear Simon, et al,
> 
> I finally got back around to working on this idea. I'm not yet quite sure 
> whether I've now understood it all. I have reread the latest edition of 
> "System F with Type Equality Coercions" (Jan 2011 version), so I understand 
> that inference is now just percolating coercions upwards, as it were, and 
> then solving the set of wanted constraints. If the set is consistent, the 
> program type-checks. This is at the core of what I have now:
> 
> 
> typeCheck :: GhcMonad m => Type -> Type -> m (Messages, Maybe (TcCoercion, 
> Bag EvBind))
> typeCheck expectedTy actualTy = do
>   let mod = mkModule mainPackageId $ mkModuleName ""
>   env <- getSession
>   liftIO $ initTc env HsSrcFile False mod $ do
> (coerce,wanted) <- captureConstraints $ do
>   (expectedWrap, expectedRho) <- deeplyInstantiate DefaultOrigin 
> expectedTy
>   (actualWrap,   actualRho  ) <- deeplyInstantiate DefaultOrigin actualTy
>   unifyType actualRho expectedRho
> binds <- simplifyTop wanted
> return (coerce,binds)
> 
> 
> It appears both the "hole" (expectedTy) and the thing to go into the hole 
> (actualTy) need to be deeply instantiated, otherwise, this function rejects 
> putting (exprType "1") into the first argument position of (exprType "(+)"), 
> because it either can't match 'a' to 'Num b => b', or (if we take the 
> rho-type), it misses 'Num b'. Anyway, deeply instantiating both seems to 
> solve such problems and, in the cases I've tried, type checks the things I 
> would expect and rejects the things I would expect.
> 
> There are two missing bits, still:
> 
> Firstly, when leaving variables ambiguous (i.e. filling a "Monad m => a -> m 
> a" shaped hole with "return", leaving 'm' ambiguous), simplifyTop fails. Is 
> it possible to allow for ambiguous variables, in roughly the same way that 
> (exprType "mapM return") works just fine? I've looked at some other 
> simplification functions (TcSimplify.*), but the lack of documentation makes 
> my guesswork somewhat random.
> 
> Secondly, is there a way in the API to find all the appropriate substitutions 
> for the variables in the *original* types (i.e. loosing the fresh variables 
> introduced by deeplyInstantiate)? Ultimately, I would really like to end up 
> with a TvSubst, or any other mapping from TyVar to Type.
> 
> Ideas?
> 
> Regards,
> Philip

Hi Philip,

As Simon has said, I have been working on implementing Agda-like holes in GHC. 
This is somewhat similar to what you've been working on, but so far I've only 
been concerned into reporting these holes to the user, and not trying to figure 
out what could fit into it. Also, I was adding it to GHC directly, not using 
the GHC API, so our approaches are quite different. But I'm hoping my 
experience might help you a little.

Could you show how simplifyTop fails, or show a bit more of you code? I wasn't 
able to get just this piece running as you described. If it is an ambiguity 
error as you say, it could just be the monomorphism restriction incorrectly 
assuming your types belong to top level declarations and rejecting them.

Regards,
Thijs Alkemade

signature.asc
Description: Message signed with OpenPGP using GPGMail
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

Hi Simon and others,

Yes, an update on our holes in GHC project was very due.

What I've been working on:

- The command line flag -XHoles and as a language pragma {-# LANGUAGE Holes #-} 
now work
- Holes print a warning message with:
- The origin of their type variables
- Their local environment
- Most of the code has been cleaned up to prepare it for submission as a patch.

As an example of the message, consider the module:

---

{-# LANGUAGE Holes #-}

test x = foldr _ x _

---

This prints:

---

[1 of 1] Compiling Main ( test2.hs, interpreted )

test2.hs:3:16: Warning:
Found hole `_' with type a0 -> b -> b
Where: `b' is a rigid type variable bound by
   the inferred type of test :: b -> b at test2.hs:3:1
   `a0' is a free type variable
In scope: x :: b

test2.hs:3:20: Warning:
Found hole `_' with type [a0]
Where: `a0' is a free type variable
In scope: x :: b
Ok, modules loaded: Main

---

The 3 currently remaining issues:

- Free type variables are not tidied consistently. For every one of these hole 
warnings, the same TidyEnv is reused, without taking the updates from the other 
holes into account. I'm pretty sure I know where this happens and how I could 
fix it.
- What I thought would be the local environment doesn't actually seem to be it. 
The holes store in their origin the result of `getLclTypeEnv' at their 
location, but as the Note [Bindings with closed types] says, the TopLevelFlag 
of these don't actually differentiate the top level from the non-top level 
bindings. I think it would be more helpful to only show the non-top level 
bindings at the hole's location, any hints about how to obtain just these would 
be appreciated.
- The holes do not have very accurate source location information, like some 
other errors have. The hole has its origin, ("test2.hs:3:16"), but somehow not 
something like: "In the expression: folder _ x _, In an equation for `test': 
test x = foldr _ x _". Help with how that is supposed to work would also be 
appreciated.

I'm attaching a patch of all my changes compared to HEAD as of about a week 
ago. All my work can also still be found on https://github.com/xnyhps/ghc.



patch.diff.gz
Description: GNU Zip compressed data


Best regards,
Thijs Alkemade

signature.asc
Description: Message signed with OpenPGP using GPGMail
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

On Sun, Feb 12, 2012 at 2:55 PM, Andres Löh  wrote:
> Hi Thijs.
>
> Sorry if this has been discussed before.
>
> In my opinion, the main advantage of Agda goals is not that the type
> of the hole itself is shown, but that you get information about all
> the locally defined identifiers and their types in the context of the
> hole. Your page doesn't seem to discuss this at all. Without that
> extra info, I don't see much purpose in the feature, though, because
> as others have indicated, it can relatively easily be simulated
> already.
>
> Cheers,
>  Andres

Hi Andres,

Thanks for your feedback. Showing everything in scope that matches or
can match the type of a hole is certainly something I am interested
in, but I'm afraid it's out of the scope of this project. I think
finding the types of the holes is a good first step that should make
this feature easier to implement later.

Best regards,
Thijs Alkemade

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

Hello all,

We've started a wiki-page discussing how this idea can be applied to GHC here:

http://hackage.haskell.org/trac/ghc/wiki/Holes

There have already been a number of people who indicated they'd want
to use this, so feel free to use the page to leave your comments about
how you'd want to use it.

Any comments on the best way to implement it are welcome too. We are
currently working with the idea of named holes[1], for which we are
not using the method mentioned in our earlier mails, but we're working
on an implementation more similar to how implicit parameters work.
I.e. generating constrains when a hole is encountered, so the same
name used multiple times will be inferred correctly. However, these
should propagate differently from implicit parameters and should not
create an error when the constraint is not in the type signature.

Regards,
Thijs Alkemade


[1] http://hackage.haskell.org/trac/ghc/wiki/Holes#Namedholes

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

On Thu, Jan 26, 2012 at 8:33 PM, Simon Peyton-Jones
 wrote:
>
> I'm sorry to be slow, but I still don't understand what you intend.  I wonder 
> whether you could give a series of examples?  Is this something to do with 
> GHCi?  Or some hypothetical IDE? Or do you expect to compile Foo.hs with some 
> holes in it, and get some output relating to the holes?   Be as concrete as 
> you possibly can.  Precisely how do you expect people to interact with the 
> system you envisage? What do they type in?  What output do they see on the 
> screen?
>
> Simon
>

The primary goal is to make this part of GHCi. Say, you're working on
a file Foo.hs in your favorite editor, and you have:

---

foo = foldr __ 0 [1..5]

---

And you have no idea what you should use at the location of the "__".
You bring up GHCi, and load it as a module:

$ ghci
GHCi, version 7.5.20120126: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> :load Foo.hs
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Found a hole at Foo.hs:1:13-14: Integer -> Integer -> Integer
...

You notice it needs a function, so you make some more changes and hit
save, so Foo.hs now contains:

---

foo = foldr (\x -> __) 0 [1..5]

---

You reload GHCi, to see if you made progress:

*Main> :r
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Found a hole at Foo.hs:1:20-21: Integer -> Integer
...

And that's it. It might help IDEs later on, but that is not our goal.

Regards,
Thijs Alkemade

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

On Thu, Jan 26, 2012 at 5:10 PM, Simon Peyton-Jones
 wrote:
>
> ...
>
> To me it looks like you get exactly the info that (I think) you want, and 
> moreover you can do that without changing the type inference engine at all.
>
> Simon


On Thu, Jan 26, 2012 at 5:26 PM, Twan van Laarhoven  wrote:
>
>
> You can do something similar right now with implicit parameters:
>
>   ...
>
> Twan
>
>

Thanks for your feedback.

Let me try to describe the goal better. The intended users are people
new to Haskell or people working with existing code they are not
familiar with. When starting with Haskell, at least in my experience,
it happens lot that you have an idea about what you need to write, but
there are some parts in the expression you're working on you don't
know yet. For example, you might have a function you want to call, but
some arguments you don't know yet how to supply. You can put
`undefined` in those places, and after that it compiles (and maybe if
you're lucky it will even run), but that will not help to figure out
what the correct thing to put there is.

This is where you would want to use a hole. Just like undefined, it
has type `a`, so it can be used anywhere (and when compiling, we
intend to turn it into an exception too), but the difference with
undefined is that after the typechecking has succeeded, you get a list
of your holes, with the type that was inferred for them, as a sort of
todo-list.

So there are certainly ways to figure out this information right now,
but the goal is to use it as feedback to the user when writing code.
Yes, it's possible to translate the expression by changing holes into
arguments of a function, but that might be problematic when that
expression is part of a module, as to properly typecheck that
expression the whole module needs to be typechecked. I have not used
them myself, but I think people learning Haskell will easily end up
shooting themselves in the foot with implicit parameters.

A more general, but different, way to achieve this goal we are
considering is: being able to use the typechecker to get more than
just the final type of an expression, but also the types of certain
subexpressions. Imagine being able to annotate an expression (for
example, with certain brackets), to say "typecheck everything, and
after that, also show me the type of this part".


As an update to my problem with Any *: I think I've found the cause.
The holes were inferred independently, not all of them at once (they
are now all passed as name_taus to simplifyInfer), and this was
happening after zonkTopDecls was already done, so all unbound type
variables had already been zapped to Any * (as that uses
emptyZonkEnv).

Regards,
Thijs Alkemade

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Holes in GHC

[Thijs Alkemade]

On Wed, Jan 25, 2012 at 5:50 PM, Iavor Diatchki
 wrote:

> So, whenever GHC infers a type `forall a. P => t` where `a` does not
> appear in `P` or `t`, it knows that the `a` does not matter, so t
> simply defaults it to `Any`.
>

Okay. Thanks for your explanation. But it's still not clear to me in
which way using "Any" instead of "a" is advantageous here (unless the
goal is simply to remove the unnecessary forall from the type
signature.) But I guess what we really need: how can we indicate the
`a` is does matter to us?

> I was just wondering if you could get the same behavior by using
> `undefined`?  For example,
>
>    :t [undefined, ()]
>    [()]
>

Yes, it typechecks the same way as undefined. However, the goal is to
find the types of all the holes in the input and present them to the
user, in, for example, a learning tool. Inserting `undefined` will
make it typecheck, but gives you no information beyond that. And, as
undefined is just a function in the Prelude, it doesn't get treated in
a special way by the typechecker. So it was considered to use
`undefined` to denote a hole, but that would require a much uglier
implementation (something like checking the Name of all HsVars in
tcExpr) than extending the syntax would.


On Wed, Jan 25, 2012 at 6:37 PM, Nicolas Frisby
 wrote:
> Have you considered the monomorphism restriction? For instance, does
>
> f () = map __ __
>
> exhibit the same problem when typechecked in a module?

Yes, it shows the same Any * types.

On Wed, Jan 25, 2012 at 6:10 PM, Simon Peyton-Jones
 wrote:
> are you or any of your colleagues at POPL? If so could talk in person.
> Simon
>

Nope.

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Holes in GHC

[Thijs Alkemade]

Hello!

As mentioned in our previous mail [1], we've been working on
introducing Agda's holes into GHC [2]. Our general approach is as
follows: we've added a hole to the syntax, denoted here by two
underscores: "__". We've introduced a new HsExpr for this, which
stores the hole's source span (as this is the only thing that a user
needs to identify the hole).

Then, we extended the local environment of the typechecker to include
a mutable Map, mapping a SrcSpan to a Type and a WantedConstraints (we
need these later to produce the correct class constraints on the
type). In TcExpr.lhs, whenever the tcExpr function encounters a hole,
it adds the source position with the res_ty and the current tcl_lie to
the map.

After type checking has finished, these types can be taken out of the
map and shown to the user, however, we are not sure yet where to do
this. Currently the map is read in tcRnModule and tcRnExpr, so loading
modules and evaluating expressions with ":t" will show the types of
the holes in that module or expression. There, we call mkPiTypes,
mkForAllTys (with the quantified type variables we obtained from the
WantedConstraints), we zonk and tidy them all (most of this imitates
how tcRnExpr modifies a type before returning it, except the tidying,
which needs to pass the updated TidyEnv to the tidying of the next
hole).

Examples:

*Main> :t [__, ()]
tcRnExpr2: [(:1:2-3, ())]
[__, ()] :: [()]

*Main> :t map __ __
tcRnExpr2: [(:1:5-6, a0 -> b), (:1:8-9, [a0])]
map __ __ :: [b]

Any feedback on this design would be appreciated. We would like to
know if this is something that could be considered to be added to GHC,
and what your requirements for that are.



Also, we have a confusing problem when type checking a module. Above,
we showed the result of ":t map __ __" in ghci. However, if we put "f
= map __ __" in a module, we get:

tcRnModule: [(f.hs:1:9-10, GHC.Prim.Any * -> b),
(f.hs:1:12-13, [GHC.Prim.Any *])]

If I read GHC.Prim.Any * as forall a. a, then this is not correct: the
GHC.Prim.Any * in both holes should have the same type. We assume it
shows up because the type that should be there does not occur in the
type signature of f (as it's just [b]), but so far we've been unable
to figure out why this behavior is different in interactive mode. Does
someone have an idea about what to do to avoid the introduction of
these GHC.Prim.Any * types?

Best regards,
Thijs Alkemade

[1] 
http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021453.html
[2] https://github.com/xnyhps/ghc/commits/master

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: Finding the type of a hole

[Thijs Alkemade]

On 5 jan. 2012, at 14:08, Sean Leather wrote:

> We're currently looking into so-called expression holes in GHC -- like the 
> type goals of Agda -- and we've run into a problem of understanding.
> 
> We have defined an expression, call it __ for now, for which we want to find 
> the type after a program is type-checked. In tcExpr (TcExpr.lhs), we can see 
> the type that arrives in the argument res_ty, but that does not appear to 
> give the correct (or final?) type after applying zonkTcType. For example, if 
> we have (__, __), then we find that both holes have some type "t" (as 
> printed). We also see this in a module with declarations such as f = __ and g 
> = __. When these are actually typed, they get unique type variables as 
> expected. So, apparently, we're missing something in trying to find the 
> proper type of a hole.
> 
> Any suggestions on what we should do or look at?
> 
> Note that we're currently working from 7.2.2, because we could not previously 
> build HEAD.
> 
> Thanks,
> Sean

As an update to this: I realized that tidying wasn't applied correctly. 
Previously each hole was typed separately using an empty tidy environment, 
causing wrong substitutions to be made. Using tidyOpenType and passing the 
updated environment for each hole has fixed the resulting type.

Regards,
Thijs

smime.p7s
Description: S/MIME cryptographic signature
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users