idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.44k stars 644 forks source link

Incorrect behaviour when resolving associated type of an interface #4918

Open casper-pragma opened 2 years ago

casper-pragma commented 2 years ago

I have defined the following interface:

interface Failable c where
  Failure : Type
  initWithFailure : Failure -> c

Then I proceeded to create an implementation:

Failable (Maybe a) where
  Failure = ({T:Type} -> T)
  initWithFailure _ = Nothing

This was accepted by the compiler, but when I tried to use it in the following manner...

main :: IO ()
main = do
  let smth : ({K:Type} -> Maybe K) = initWithFailure ()

...the compiler said that there is a type mismatch between () and Failure.

This not suppose to happen, right?