ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

"RefType.refAppTyToFun" error #2381

Open gergoerdi opened 1 month ago

gergoerdi commented 1 month ago

I'm getting an "Uh oh" error on the following standalone input file on 5595507d943cb00f92674c19a5cbafcd93dff92b:

{-# LANGUAGE NoImplicitPrelude #-}
module Arrow where

infixr 3 >>>
infixr 3 ***
infixr 3 &&&

class Arrow a where
    (>>>) :: a b c -> a c d -> a b d

    arr :: (b -> c) -> a b c

    (***) :: a b c -> a b' c' -> a (b,b') (c,c')

    (&&&) :: a b c -> a b c' -> a b (c,c')
    f &&& g = arr (\b -> (b,b)) >>> f *** g

instance Arrow (->) where
    f >>> g = \x -> g (f x)
    arr f = f
    (f *** g) (x,y) = (f x, g y)

The exact output of LH is:

[1 of 1] Compiling Arrow            ( input/Arrow.hs, input/Arrow.o )
<no location info>: error: Uh oh.
    RefType.refAppTyToFun
gergoerdi commented 1 month ago

I have stumbled upon a much simpler reproducer:

{-# LANGUAGE NoImplicitPrelude #-}
module Exceptions (main) where

mustThrow :: forall p exc. p exc -> ()
mustThrow _ = ()

main :: ()
main = mustThrow (\x -> ())