Skip to content

Instantly share code, notes, and snippets.

@witt3rd

witt3rd/infunif.idr

Last active October 10, 2020 16:31
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save witt3rd/6543b6bfdb8cea3705a0d20d9d7dfc47 to your computer and use it in GitHub Desktop.
Save witt3rd/6543b6bfdb8cea3705a0d20d9d7dfc47 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
infunif.idr
data Foo a = Bar a
| Baz (Foo a) (Foo a)
fooEq : DecEq a => a -> a -> Foo a -> Foo a -> Maybe (Foo a)
fooEq x y f g = case decEq x y of
Yes _ => Just (Baz f g)
No _ => Nothing
comb : DecEq a => Foo a -> Foo a -> Maybe (Foo a)
comb f@(Bar x ) g@(Bar y ) = fooEq x y f g -- < ok
comb f@(Bar x ) g@(Baz y z) = fooEq x y f g -- < error
comb f@(Baz x z) g@(Bar y ) = fooEq x y f g -- < error
comb f@(Baz x z) g@(Baz y w) = fooEq x y f g -- < error
{-
When checking right hand side of comb with expected type
Maybe (Foo a)
When checking an application of function Main.fooEq:
Unifying a and Foo a would lead to infinite value
-}
@witt3rd
Copy link
Author

witt3rd commented Oct 10, 2020 

data Foo a = Bar a
           | Baz (Foo a) (Foo a)

fooEq : DecEq a => a -> a -> Foo a -> Foo a -> Maybe (Foo a)
fooEq x y f g = case decEq x y of
  Yes _ => Just (Baz f g)
  No  _ => Nothing

comb : DecEq a => Foo a -> Foo a -> Maybe (Foo a)
comb f@(Bar x)           g@(Bar y)           = fooEq x y f g
comb f@(Bar x)           g@(Baz (Bar y) _)   = fooEq x y f g
comb f@(Baz _ (Bar x))   g@(Bar y)           = fooEq x y f g
comb f@(Baz _ (Bar x))   g@(Baz (Bar y) _)   = fooEq x y f g
comb f                     (Baz (Baz g _) _) = comb f g
comb f@(Baz _ (Baz h _)) g                   = comb f g
comb   (Baz _ (Baz f _))   (Baz (Baz g _) _) = comb f g

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment